Library Stdlib.Zmod.ZmodInv

From Stdlib Require Import ZArith ZModOffset Zcong Lia Field_theory.
From Stdlib Require Import Bool.Bool Lists.List Lists.Finite Sorting.Permutation.
Import ListNotations.

From Stdlib Require Import Zmod.ZmodDef Zmod.ZstarDef Zmod.ZmodBase Zmod.ZstarBase.
Local Open Scope Z_scope.
Local Coercion ZmodDef.Zmod.to_Z : Zmod >-> Z.
Local Coercion Zstar.to_Zmod : Zstar.Zstar >-> Zmod.Zmod.

Local Hint Extern 0 (?x <-> ?x) => reflexivity : core.

Module Zmod.
Import ZstarDef.Zstar ZstarBase.Zstar ZmodDef.Zmod ZmodBase.Zmod.

Lemma mdiv_same [m] (a : Zmod m) : mdiv a a = of_Z m (Z.gcd a m).

Lemma in_invertibles [m] (x : Zmod m) : List.In x (invertibles m) <-> Z.coprime x m.
Lemma NoDup_invertibles m : List.NoDup (invertibles m).

Lemma mdiv_same_coprime [m] (a : Zmod m) (H : Z.gcd a m = 1) : mdiv a a = one.

Lemma mdiv_same_prime [m] (x : Zmod m) (Hm : Z.prime m) (H : x <> zero) : mdiv x x = one.

Lemma mul_inv_same_l_coprime [m] (x : Zmod m) (H : Z.gcd x m = 1) :
  mul (inv x) x = one.

Lemma mul_inv_same_r_coprime [m] (x : Zmod m) (H : Z.gcd x m = 1) :
  mul x (inv x) = one.

Lemma mul_inv_same_l_prime [m] (x : Zmod m) (Hm : Z.prime m) (H : x <> zero) :
  mul (inv x) x = one.

Lemma mul_inv_same_r_prime [m] (x : Zmod m) (Hm : Z.prime m) (H : x <> zero) :
  mul x (inv x) = one.

Lemma field_theory m (Hm : Z.prime m) :
  @field_theory (Zmod m) zero one add mul sub opp mdiv inv eq.

Lemma inv_nz_prime [m] (x : Zmod m) (Hm : Z.prime m) (Hx : x <> zero) : inv x <> zero.

Lemma inv_inv [m] (x : Zmod m) (H : Z.gcd x m = 1): inv (inv x) = x.

Lemma inv_inv_prime [m] (x : Zmod m) (Hm : Z.prime m): inv (inv x) = x.

Lemma inv_1 m : @inv m one = one.

Lemma div_1_r [m] x : @mdiv m x one = x.

Lemma mul_cancel_l_coprime [m] (a b c : Zmod m)
  (Ha : Z.gcd a m = 1) (H : mul a b = mul a c) : b = c.

Lemma mul_cancel_r_coprime [m] (a b c : Zmod m)
  (Ha : Z.gcd a m = 1) (H : mul b a = mul c a) : b = c.

Lemma mul_cancel_l_prime [m] (a b c : Zmod m) (Hm : Z.prime m) (Ha : a <> zero)
  (H : mul a b = mul a c) : b = c.

Lemma mul_0_iff_prime [p] (Hp : Z.prime p) (a b : Zmod p) :
  mul a b = zero <-> a = zero \/ b = zero.

Lemma pow_succ_r_coprime [m] (x : Zmod m) z (H : Z.gcd x m = 1) : pow x (Z.succ z) = mul x (pow x z).

Lemma pow_pred_r_coprime [m] (x : Zmod m) z (H : Z.gcd x m = 1) : pow x (Z.pred z) = mdiv (pow x z) x.

Lemma pow_add_r_coprime [m] (x : Zmod m) a b (H : Z.gcd x m = 1) : pow x (a + b) = mul (pow x a) (pow x b).

Lemma pow_mul_r_coprime [m] (x : Zmod m) a b (H : Z.gcd x m = 1) : pow x (a * b) = pow (pow x a) b.

Lemma pow_mul_l_coprime [m] (x y : Zmod m) z (Hx : Z.gcd x m = 1) (Hy : Z.gcd y m = 1) :
  pow (mul x y) z = mul (pow x z) (pow y z).

Lemma pow_1_l [m] z : @pow m one z = one.

Lemma pow_mul_r_nonneg [m] (x : Zmod m) a b (Ha : 0 <= a) (Hb : 0 <= b) :
  pow x (a*b) = pow (pow x a) b.

Lemma square_roots_opp_prime [p] (Hp : Z.prime p) (x y : Zmod p) :
  pow x 2 = pow y 2 <-> (x = y \/ x = opp y).

Lemma square_roots_1_prime [p] (Hp : Z.prime p) (x : Zmod p) :
  pow x 2 = one <-> (x = one \/ x = opp one).

Lemma mul_cancel_r_prime [m] (a b c : Zmod m) (Hm : Z.prime m) (Ha : a <> zero)
  (H : mul b a = mul c a) : b = c.

Theorem fermat_nz [m] (a : Zmod m) (Ha : a <> zero) (H : Z.prime m) :
  pow a (Z.pred m) = one.

Theorem fermat [m] (a : Zmod m) (H : Z.prime m) : pow a m = a.
Theorem fermat_inv [m] (a : Zmod m) (Ha : a <> zero) (H : Z.prime m) :
  pow a (m-2) = inv a.
End Zmod.

Module Z.
Import Znumtheory.

Theorem fermat_nz (m a : Z) (Hm : Z.prime m) (Ha : a mod m <> 0) :
  a^(m-1) mod m = 1.

Theorem fermat (m a : Z) (Hm : Z.prime m) : a^m mod m = a mod m.
End Z.