Library Stdlib.Zmod.ZmodBase

From Stdlib Require Import BinNat BinInt Znat PreOmega Lia Ring ZArith_dec.
From Stdlib Require Import Wf_Z Zdiv Zdiv_facts Zdivisibility ZModOffset Zcong.
From Stdlib Require Import Bool.Bool Lists.List Sorting.Permutation.
From Stdlib Require Import Zmod.ZmodDef.
Import ListNotations.

Local Open Scope Zmod_scope.
Local Open Scope Z_scope.

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

Module Zmod.
Export ZmodDef.Zmod.

Local Lemma small_iff z m :
  Bool.Is_true (ZmodDef.Zmod.small z m) <-> z mod m = z.

Lemma mod_unsigned [m] (x : Zmod m) : x mod m = x.
Notation mod_to_Z := mod_unsigned (only parsing).

Lemma unsigned_range [m] (x : Zmod m) : 0 <= x < m \/ m = 0 \/ m < x <= 0.
Notation to_Z_range := unsigned_range (only parsing).

Lemma unsigned_pos_bound [m] (x : Zmod m) : 0 < m -> 0 <= x < m.
Notation to_Z_pos_bound := unsigned_pos_bound (only parsing).

Lemma unsigned_neg_bound [m] (x : Zmod m) : m < 0 -> m < x <= 0.
Notation to_Z_neg_bound := unsigned_neg_bound (only parsing).

Lemma unsigned_inj m (x y : Zmod m) : to_Z x = to_Z y -> x = y.
Notation to_Z_inj := unsigned_inj (only parsing).

Lemma unsigned_inj_iff [m] (x y : Zmod m) : to_Z x = to_Z y <-> x = y.
Notation to_Z_inj_iff := unsigned_inj_iff (only parsing).

Lemma unsigned_of_small_Z [m] z (H : z mod m = z) : to_Z (of_small_Z m z) = z.
Notation to_Z_of_small_Z := unsigned_of_small_Z (only parsing).

Lemma unsigned_of_Z [m] z : to_Z (of_Z m z) = z mod m.
Notation to_Z_of_Z := unsigned_of_Z (only parsing).

Lemma of_small_Z_ok [m] z (H : z mod m = z) : of_small_Z m z = of_Z m z.

Lemma of_Z_unsigned [m] x : of_Z m (unsigned x) = x.
Notation of_Z_to_Z := of_Z_unsigned (only parsing).

Lemma unsigned_of_Z_id_iff [m] n :
  to_Z (of_Z m n) = n <-> 0 <= n < m \/ m = 0 \/ m < n <= 0.
Notation to_Z_of_Z_id_iff := unsigned_of_Z_id_iff.

Lemma unsigned_of_Z_id [m] n (H : 0 <= n < m \/ m = 0 \/ m < n <= 0) :
  to_Z (of_Z m n) = n.
Notation to_Z_of_Z_id := unsigned_of_Z_id .

Lemma unsigned_of_Z_mod0 n : to_Z (of_Z 0 n) = n.
Notation to_Z_of_Z_mod0 := unsigned_of_Z_mod0 (only parsing).

Lemma unsigned_of_Z_small [m] n (H : 0 <= n < m) : to_Z (of_Z m n) = n.
Notation to_Z_of_Z_small := unsigned_of_Z_small.

Lemma of_Z_mod [m] x : of_Z m (x mod m) = of_Z m x.

Lemma of_Z_mod_abs [m] x : of_Z m (x mod (Z.abs m)) = of_Z m x.

Lemma of_Z_inj [m] x y : of_Z m x = of_Z m y <-> x mod m = y mod m.
Lemma of_Z_inj_abs' [m] x y : of_Z m x = of_Z m y <-> x mod (Z.abs m) = y mod (Z.abs m).

Lemma of_Z_inj_abs [m] x y : of_Z m x = of_Z m y <-> (Z.abs m <> 1 -> x mod (Z.abs m) = y mod (Z.abs m)).

Lemma of_Z_inj_cases [m] x y : of_Z m x = of_Z m y <->
  ((m = 0 -> x = y) /\ let m' := Z.abs m in 2 <= m' -> x mod m' = y mod m').

Lemma smod_unsigned [m] (x : Zmod m) : Z.smodulo (unsigned x) m = signed x.

Lemma smod_signed [m] (x : Zmod m) : Z.smodulo (signed x) m = signed x.

Lemma signed_inj m (x y : Zmod m) : signed x = signed y -> x = y.

Lemma signed_inj_iff [m] (x y : Zmod m) : signed x = signed y <-> x = y.

Lemma mod_signed [m] (x : Zmod m) : signed x mod m = unsigned x.

Lemma signed_of_Z [m] z : signed (of_Z m z) = Z.smodulo z m.

Lemma signed_eq_unsigned_iff [m] x :
  @signed m x = unsigned x <-> 2*Z.abs x < Z.abs m \/ m = 0.

Lemma signed_eq_unsigned [m] (x : Zmod m) :
  2*Z.abs x < Z.abs m \/ m = 0 -> signed x = unsigned x.

Lemma signed_of_Z_mod0 n : signed (of_Z 0 n) = n.

Lemma signed_of_Z_id_iff m z :
  signed (of_Z m z) = z <->
  - m <= 2 * z - Z.rem m 2 < m \/ m = 0 \/ m < 2 * z - Z.rem m 2 <= - m.

Lemma signed_of_Z_id m z :
  - m <= 2 * z - Z.rem m 2 < m \/ m = 0 \/ m < 2 * z - Z.rem m 2 <= - m ->
  signed (of_Z m z) = z.

Lemma signed_cases [m] (x : Zmod m) :
  signed x = unsigned x /\ 2*Z.abs x < Z.abs m \/
  signed x = unsigned x - m /\ Z.abs m <= 2*Z.abs x.

Lemma signed_of_Z_small [m] z (H : - m <= 2 * z - Z.rem m 2 < m) :
  signed (of_Z m z) = z.

Lemma signed_of_Z_even_small [m] (Hm : m mod 2 = 0)
  z (H : - m <= 2 * z < m) : signed (of_Z m z) = z.

Lemma of_Z_signed [m] x : of_Z m (signed x) = x.

Lemma signed_range [m] (x : Zmod m) :
  ltac:(let t := type of (Z.smod_small_iff (signed x) m) in
  match eval cbv zeta in t with ?P <-> _ => exact P end).

Lemma signed_pos_bound [m] (x : Zmod m) (Hm : 0 < m) : -m <= 2*signed x < m.

Lemma signed_neg_bound [m] (x : Zmod m) (Hm : m < 0) : m < 2*signed x <= - m.

Lemma signed_small [m] (x : Zmod m) (H : 0 <= 2*x < m) : signed x = unsigned x.

Lemma signed_large [m] (x : Zmod m) (H : 0 <= m <= 2*x) : signed x = x-m.

Lemma unsigned_pos [m] (x : Zmod m) (Hm : 0 <= m) (H : 0 <= signed x) : unsigned x = signed x.
Notation to_Z_pos := unsigned_pos (only parsing).

Lemma unsigned_neg [m] (x : Zmod m) (Hm : 0 <= m) (H : signed x < 0) : unsigned x = m + signed x.
Notation to_Z_neg := unsigned_neg (only parsing).

Lemma signed_neg_iff [m] (x : Zmod m) :
  signed x < 0 <-> 0 < m <= 2*x \/ m = 0 /\ x < 0 \/ m < 2*x < 0.

Lemma signed_pos_iff [m] (x : Zmod m) :
  0 < signed x <-> 0 < 2*x < m \/ m = 0 /\ 0 < x \/ 2*x <= m < 0.

Lemma signed_nonneg_iff [m] (x : Zmod m) :
  0 <= signed x <-> 0 <= 2*x < m \/ m = 0 /\ 0 <= x \/ (m < 0 /\ (2*x <= m \/ 0 = x)).

Lemma signed_small_iff [m] (x : Zmod m) (Hm : 0 < m) :
  signed x = x <-> 2*x < m.

Lemma unsigned_0 m : @to_Z m zero = 0.
Notation to_Z_0 := unsigned_0 (only parsing).

Lemma unsigned_0_iff [m] x : @to_Z m x = 0 <-> x = zero.
Notation to_Z_0_iff := unsigned_0_iff (only parsing).

Lemma of_Z_0 m : of_Z m 0 = zero.

Lemma signed_0 m : @signed m zero = 0.

Lemma signed_0_iff [m] x : @signed m x = 0 <-> x = zero.

Lemma of_Z_1 m : of_Z m 1 = one.

Lemma unsigned_1 m : @to_Z m one = 1 mod m.
Notation to_Z_1 := unsigned_1 (only parsing).

Lemma unsigned_1_pos [m] (Hm : 2 <= m) : @to_Z m one = 1.
Notation to_Z_1_pos := unsigned_1_pos (only parsing).

Lemma unsigned_1_1 : @to_Z 1 one = 0.
Notation to_Z_1_1 := unsigned_1_1 (only parsing).

Lemma unsigned_1_neg [m] (Hm : m <= 0) : @to_Z m one = m+1.
Notation to_Z_1_neg := unsigned_1_neg (only parsing).

Lemma unsigned_1_cases m : @to_Z m one =
  if 2 <=? m then 1 else if m =? 1 then 0 else m+1.
Notation to_Z_1_cases := unsigned_1_cases (only parsing).

Lemma gcd_1_m m : Z.coprime (@one m) m.

Lemma signed_1 [m] (Hm : 3 <= m) : @signed m one = 1.

Lemma signed_1_1 : @signed 1 one = 0.

Lemma signed_1_2 : @signed 2 one = -1.

Lemma unsigned_nz [m] (x : Zmod m) (H : x <> zero) : to_Z x <> 0.
Notation to_Z_nz := unsigned_nz (only parsing).

Lemma one_eq_zero_mod_1 : @one 1 = zero.

Lemma one_eq_zero_iff m : one = zero :> Zmod m <-> Z.abs m = 1.

Lemma one_neq_zero [m] (Hm : 2 <= Z.abs m) : one <> zero :> Zmod m.

Lemma of_Z_nz [m] x (H : x mod m <> 0) : of_Z m x <> zero.

Lemma hprop_Zmod_1 (a b : Zmod 1) : a = b.

Lemma hprop_Zmod_m1 (a b : Zmod (-1)) : a = b.

Lemma unsigned_Zmod1 (a : Zmod 1) : to_Z a = 0.
Notation to_Z_Zmod1 := unsigned_Zmod1 (only parsing).

Lemma unsigned_Zmodm1 (a : Zmod (-1)) : to_Z a = 0.
Notation to_Z_Zmodm1 := unsigned_Zmodm1 (only parsing).

Lemma signed_Zmod1 (a : Zmod 1) : signed a = 0.

Lemma signed_Zmodm1 (a : Zmod (-1)) : signed a = 0.

Lemma wlog_eq_Zmod_2_pos [m] (a b : Zmod m) (Hm : 0 < m) (k : 2 <= m -> a = b) : a = b.
Lemma wlog_eq_Zmod_2_neg [m] (a b : Zmod m) (Hm : m < 0) (k : m <= -2 -> a = b) : a = b.
Lemma wlog_eq_Zmod_2_abs [m] (a b : Zmod m) (k : m = 0 \/ 2 <= Z.abs m -> a = b) : a = b.

Lemma unsigned_add [m] (x y : Zmod m) : to_Z (x + y) = (to_Z x + to_Z y) mod m.
Notation to_Z_add := unsigned_add (only parsing).

Lemma eqb_spec [m] (x y : Zmod m) : BoolSpec (x = y) (x <> y) (eqb x y).

Lemma eqb_eq [m] (x y : Zmod m) : eqb x y = true <-> x = y.

Lemma eqb_refl [m] (x : Zmod m) : eqb x x = true.

Lemma signed_add [m] x y : signed (@add m x y) = Z.smodulo (signed x+signed y) m.

Lemma of_Z_add [m] (x y : Z) : of_Z m (Z.add x y) = add (of_Z m x) (of_Z m y).

Lemma unsigned_sub [m] (x y : Zmod m) : to_Z (x - y) = (to_Z x - to_Z y) mod m.
Notation to_Z_sub := unsigned_sub (only parsing).

Lemma signed_sub [m] x y : signed (@sub m x y) = Z.smodulo (signed x-signed y) m.

Lemma of_Z_sub [m] (x y : Z) : of_Z m (Z.sub x y) = sub (of_Z m x) (of_Z m y).

Lemma unsigned_opp [m] (x : Zmod m) : to_Z (opp x) = (- to_Z x) mod m.
Notation to_Z_opp := unsigned_opp (only parsing).

Lemma signed_opp [m] x : signed (@opp m x) = Z.smodulo (-signed x) m.

Lemma unsigned_m1 m : @to_Z m (opp one) = -1 mod m.

Lemma unsigned_m1_pos [m : Z] (H : 2 <= m) : @to_Z m (opp one) = m-1.
Notation to_Z_m1_pos := unsigned_m1_pos (only parsing).

Lemma unsigned_m1_1 : @to_Z 1 (opp one) = 0.
Notation to_Z_m1_1 := unsigned_m1_1 (only parsing).

Lemma unsigned_m1_m1 : @to_Z (-1) (opp one) = 0.
Notation to_Z_m1_m1 := unsigned_m1_m1 (only parsing).

Lemma unsigned_m1_neg [m : Z] (H : m <= -2) : @to_Z m (opp one) = -1.
Notation to_Z_m1_neg := unsigned_m1_neg (only parsing).

Lemma unsigned_m1_cases m : @to_Z m (opp one) =
  if (m <=? -2) || (m =? 0) then -1
  else if Z.abs m =? 1 then 0
  else m-1.
Notation to_Z_m1_cases := unsigned_m1_cases (only parsing).

Lemma of_Z_m1 m : @of_Z m (-1) = opp one.

Lemma signed_m1 [m] (Hm : 2 <= m) : @signed m (opp one) = -1.

Lemma of_Z_opp [m] (x : Z) : of_Z m (Z.opp x) = opp (of_Z m x).

Lemma opp_zero m : @opp m zero = zero.

Lemma opp_overflow [m] (Hm : m mod 2 = 0)
  (x : Zmod m) (Hx : signed x = -m/2) : opp x = x.

Lemma signed_opp_odd [m] (x : Zmod m) (H : m mod 2 = 1) :
  signed (opp x) = Z.opp (signed x).

Lemma signed_opp_small [m] (x : Zmod m) (H : signed x = -m/2 -> m mod 2 = 1) :
  signed (- x) = Z.opp (signed x).

Lemma unsigned_mul [m] (x y : Zmod m) : to_Z (x * y) = (to_Z x * to_Z y) mod m.
Notation to_Z_mul := unsigned_mul (only parsing).

Lemma signed_mul [m] x y : signed (@mul m x y) = Z.smodulo (signed x*signed y) m.

Lemma of_Z_mul [m] (x y : Z) : of_Z m (Z.mul x y) = mul (of_Z m x) (of_Z m y).

Local Ltac r := try apply to_Z_inj; cbv [one];
  
  repeat rewrite ?to_Z_of_Z, ?to_Z_add, ?to_Z_mul, ?to_Z_sub, ?to_Z_opp,
    ?mod_to_Z, ?Zmod_0_l, ?Z.mul_1_l, ?Z.add_0_l, ?Zplus_mod_idemp_l,
    ?Zplus_mod_idemp_r, ?Zmult_mod_idemp_l, ?Zmult_mod_idemp_r,
    ?Z.add_opp_diag_r, ?to_Z_0;
  try (f_equal; lia).

Lemma add_0_l [m] a : @add m zero a = a.
Lemma add_comm [m] a b : @add m a b = add b a.
Lemma mul_comm [m] a b : @mul m a b = mul b a.
Lemma add_assoc [m] a b c : @add m a (add b c) = add (add a b) c.
Lemma mul_assoc [m] a b c : @mul m a (mul b c) = mul (mul a b) c.
Lemma mul_add_l [m] a b c : @mul m (add a b) c = add (mul a c) (mul b c).
Lemma mul_1_l [m] a : @mul m one a = a.
Lemma add_opp_r [m] a b : @add m a (opp b) = sub a b.
Lemma add_opp_same_r [m] a : @add m a (opp a) = zero.

Lemma sub_same [m] a : @sub m a a = zero.

Lemma ring_theory m : @ring_theory (Zmod m) zero one add mul sub opp eq.

Section WithRing.
  Context [m : Z].
  Add Ring __Private__Zmod_base_ring : (ring_theory m).
  Implicit Types a b c : Zmod m.
  Lemma opp_0 : opp zero = zero :> Zmod m.
  Lemma add_0_r a : add a zero = a.
  Lemma sub_0_l a : sub zero a = opp a.
  Lemma sub_0_r a : sub a zero = a.
  Lemma mul_1_r a : mul a one = a.
  Lemma mul_m1_l a : mul (opp one) a = opp a.
  Lemma mul_m1_r a : mul a (opp one) = opp a.
  Lemma mul_0_l a : mul zero a = zero.
  Lemma mul_0_r a : mul a zero = zero.
  Lemma opp_opp a : opp (opp a) = a.
  Lemma opp_inj a b : opp a = opp b -> a = b.
  Lemma opp_inj_iff a b : opp a = opp b <-> a = b.
  Lemma add_opp_l a b : add (opp a) b = sub b a.
  Lemma sub_opp_r a b : sub a (opp b) = add a b.
  Lemma sub_opp_l a b : sub (opp a) b = opp (add a b).
  Lemma add_sub_r a b c : add a (sub b c) = sub (add a b) c.
  Lemma add_sub_l a b c : add (sub a b) c = sub (add a c) b.
  Lemma sub_sub_r a b c : sub a (sub b c) = sub (add a c) b.
  Lemma sub_sub_l a b c : sub (sub a b) c = sub a (add b c).
  Lemma mul_add_r a b c : mul a (add b c) = add (mul a b) (mul a c).
  Lemma add_opp_same_l a : @add m (opp a) a = zero.
  Lemma mul_sub_l a b c : mul (sub a b) c = sub (mul a c) (mul b c).
  Lemma mul_sub_r a b c : mul a (sub b c) = sub (mul a b) (mul a c).
  Lemma mul_opp_l a b : mul (opp a) b = opp (mul a b).
  Lemma mul_opp_r a b : mul a (opp b) = opp (mul a b).
  Lemma mul_opp_opp a b : mul (opp a) (opp b) = mul a b.
  Local Lemma square_roots_opp_prime_subproof a b :
    sub (mul a a) (mul b b) = mul (sub a (opp b)) (sub a b).
End WithRing.

Lemma udiv_0_r [m] x : @udiv m x zero = opp one.

Lemma unsigned_udiv [m] (x y : Zmod m) (Hy : y <> 0 :> Z) : to_Z (@udiv m x y) = Z.div x y mod m.
Notation to_Z_udiv := unsigned_udiv (only parsing).

Lemma unsigned_udiv_nonneg [m] (x y : Zmod m) (Hm : 0 <= m) (Hy : y <> 0 :> Z) : to_Z (@udiv m x y) = Z.div x y.
Notation to_Z_udiv_nonneg := unsigned_udiv_nonneg (only parsing).

Lemma of_Z_div_small [m] (x y : Z) (Hx : 0 <= x < m) (Hy : 0 < y < m) :
  of_Z m (x / y) = udiv (of_Z _ x) (of_Z _ y).

Lemma unsigned_umod [m] x y : to_Z (@umod m x y) = Z.modulo x y.
Notation to_Z_umod := unsigned_umod (only parsing).

Lemma of_Z_umod_small [m] (x y : Z) (Hx : 0 <= x < m) (Hy : 0 <= y < m) :
  of_Z m (x mod y) = umod (of_Z _ x) (of_Z _ y).

Lemma umod_0_r [m] x : @umod m x zero = x.

Lemma signed_squot [m] x y : @signed m (squot x y) =
  Z.smodulo (if signed y =? 0 then -1 else signed x ÷ signed y) m.

Lemma signed_squot_nz [m] x y : signed y <> 0 -> @signed m (squot x y) = Z.smodulo (signed x ÷ signed y) m.

Lemma signed_srem [m] x y : @signed m (srem x y) = Z.smodulo (Z.rem (signed x) (signed y)) m.

Lemma squot_0_r [m] x : @squot m x zero = opp one.

Lemma smod_0_r [m] x : @srem m x zero = x.

Lemma signed_squot_small [m] x y (Hm : 0 <= m) (Hy : signed y <> 0) :
  ~ (signed x = -m/2 /\ signed y = -1 /\ m mod 2 = 0) ->
  @signed m (squot x y) = signed x ÷ signed y.

Lemma squot_overflow [m] x y
  (Hm : m mod 2 = 0) (Hx : signed x = -m/2) (Hy : signed y = -1) :
  @squot m x y = x.

Lemma squot_m1_r [m] (x : Zmod m) (Hm : 0 < m) : @squot m x (opp one) = opp x.

Lemma unsigned_inv [m] x : to_Z (@inv m x) = Z.invmod x m.
Notation to_Z_inv := unsigned_inv (only parsing).

Lemma inv_0 m : @inv m zero = zero.

Lemma unsigned_mdiv [m] x y : to_Z (@mdiv m x y) = x * Z.invmod y m mod m.
Notation to_Z_mdiv := unsigned_mdiv (only parsing).

Lemma mdiv_0_r [m] x : @mdiv m x zero = zero.

Lemma mul_inv_l [m] x y : mul (@inv m y) x = mdiv x y.

Lemma mul_inv_r [m] x y : mul x (@inv m y) = mdiv x y.

Lemma unsigned_and [m] x y : @to_Z m (and x y) = Z.land x y mod m.
Notation to_Z_and := unsigned_and (only parsing).

Lemma unsigned_and_small [m] (Hm : 0 <= m) x y : @to_Z m (and x y) = Z.land x y.
Notation to_Z_and_small := unsigned_and_small (only parsing).

Lemma unsigned_ndn [m] x y : @to_Z m (ndn x y) = Z.ldiff x y mod m.
Notation to_Z_ndn := unsigned_ndn (only parsing).

Lemma unsigned_ndn_small [m] x y (Hm : 0 <= m) : @to_Z m (ndn x y) = Z.ldiff x y.
Notation to_Z_ndn_small := unsigned_ndn_small (only parsing).

Lemma unsigned_slu [m] x n : @to_Z m (slu x n) = Z.shiftl x n mod m.
Notation to_Z_slu := unsigned_slu (only parsing).

Lemma unsigned_sru [m] x n (Hn : 0 <= n) : @to_Z m (sru x n) = Z.shiftr x n.
Notation to_Z_sru := unsigned_sru (only parsing).

Lemma signed_srs [m] x n (Hn : 0 <= n) : @signed m (srs x n) = Z.shiftr (signed x) n.

Lemma unsigned_srs [m] x n (Hn : 0 <= n) : @to_Z m (srs x n) = Z.shiftr (signed x) n mod m.
Notation to_Z_srs := unsigned_srs (only parsing).

Lemma sru_neg_r [m] (x :Zmod m) n (Hn : n <= 0) : sru x n = slu x (-n).

Lemma srs_neg_r [m] (x :Zmod m) n (Hn : n <= 0) : srs x n = slu x (-n).

Lemma unsigned_inj_dep [m] (a : Zmod m) [n] (b : Zmod n) :
  m = n -> to_Z a = to_Z b -> existT _ _ a = existT _ _ b.
Notation to_Z_inj_dep := unsigned_inj_dep (only parsing).

Lemma unsigned_inj_dep_iff [m] (a : Zmod m) [n] (b : Zmod n) :
  m = n /\ to_Z a = to_Z b <-> existT _ _ a = existT _ _ b.
Notation to_Z_inj_dep_iff := unsigned_inj_dep_iff (only parsing).

Lemma unsigned_eq_rect [m] (a : Zmod m) n p : to_Z (eq_rect _ _ a n p) = to_Z a.
Notation to_Z_eq_rect := unsigned_eq_rect (only parsing).

Lemma signed_inj_dep [m] (a : Zmod m) [n] (b : Zmod n) :
  m = n -> signed a = signed b -> existT _ _ a = existT _ _ b.

Lemma signed_inj_dep_iff [m] (a : Zmod m) [n] (b : Zmod n) :
  m = n /\ signed a = signed b <-> existT _ _ a = existT _ _ b.

Lemma signed_eq_rect [m] (a : Zmod m) n p : signed (eq_rect _ _ a n p) = signed a.

Lemma eq_rect_alt [m] (a : Zmod m) n p : eq_rect _ _ a n p = of_Z _ (to_Z a).

Lemma pow_0_r [m] x : @pow m x 0 = one.

Lemma pow_1_r [m] x : @pow m x 1 = x.

Lemma pow_2_r [m] x : @pow m x 2 = mul x x.

Local Notation pow_N := ZmodDef.Zmod.Private_pow_N.

Lemma Private_pow_nonneg [m] (x : Zmod m) z (Hz : 0 <= z) : pow x z = pow_N x (Z.to_N z).

Lemma Private_pow_neg [m] (x : Zmod m) z (Hz : z < 0) : pow x z = inv (pow_N x (Z.to_N (-z))).

Lemma pow_neg [m] (x : Zmod m) z (Hz : z < 0) : pow x z = inv (pow x (-z)).

Lemma Private_pow_N_correct [m] a n : @pow_N m a n = N.iter n (mul a) one.

Lemma Private_pow_N_0_r [m] (x : Zmod m) : @pow_N m x 0 = one.

Lemma Private_pow_N_succ_r [m] (x : Zmod m) n : pow_N x (N.succ n) = mul x (pow_N x n).

Lemma pow_succ_nonneg_r [m] (x : Zmod m) n (H : 0 <= n) : pow x (Z.succ n) = mul x (pow x n).
Notation pow_succ_r_nonneg := pow_succ_nonneg_r.

Lemma pow_add_r_nonneg [m] (x : Zmod m) a b (Ha : 0 <= a) (Hb : 0 <= b) :
  pow x (a+b) = mul (x^a) (x^b).

Lemma pow_mul_l_nonneg {m} (x y : Zmod m) n (Hn : 0 <= n) :
  pow (x * y) n = mul (x ^ n) (y ^ n).

Local Coercion Z.of_N : N >-> Z.
Lemma Private_to_Z_pow_N [m] x n : @to_Z m (pow_N x n) = to_Z x ^ n mod m.

Lemma unsigned_pow_nonneg_r [m] x z (Hz : 0 <= z) : @to_Z m (pow x z) = x^z mod m.
Notation to_Z_pow_nonneg_r := unsigned_pow_nonneg_r (only parsing).

Lemma unsigned_pow_neg_r [m] x z (Hz : z < 0) : @to_Z m (pow x z) = Z.invmod (to_Z x^(-z)) m.
Notation to_Z_pow_neg_r := unsigned_pow_neg_r (only parsing).

Lemma signed_pow_nonneg_r [m] x z (Hz : 0 <= z) : @signed m (pow x z) = Z.smodulo (signed x ^ z) m.
Notation signed_pow_nonneg := signed_pow_nonneg_r.

Lemma of_Z_pow [m] x n (H : 0 <= n) : of_Z m (x ^ n) = pow (of_Z m x) n.

Lemma Private_pow_N_0_l [m] n (Hn : n <> 0%N) : @pow_N m zero n = zero.

Lemma pow_0_l [m] n (Hn : n <> 0) : @pow m zero n = zero.

Lemma sub_eq_0 [m] a b (H : @sub m a b = zero) : a = b.

Lemma sub_eq_0_iff [m] a b : @sub m a b = zero <-> a = b.

Lemma add_eq_0 [m] a b (H : @add m a b = zero) : b = opp a.

Lemma add_eq_0_iff [m] a b : @add m a b = zero <-> b = opp a.

Lemma opp_1_neq_1 [m] (Hm : 3 <= Z.abs m) : @opp m one <> one.

Lemma inv_1 m : @inv m one = one.

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

Lemma abs_0 m : @abs m zero = zero.

Lemma abs_1 m : @abs m one = one.

Lemma abs_nonneg [m] x : 0 <= @signed m x -> abs x = x.

Lemma abs_neg [m] x : @signed m x < 0 -> abs x = opp x.

Lemma abs_pos [m] x : 0 < @signed m x -> abs x = x.

Lemma abs_opp [m] x : @abs m (opp x) = abs x.

Lemma abs_abs [m] (x : Zmod m) : abs (abs x) = abs x.

Lemma signed_abs_small [m] x (H : signed x <> - m / 2) :
  @signed m (abs x) = Z.abs (signed x).

Lemma signed_abs_odd [m] (Hm : m mod 2 = 1) x :
  @signed m (abs x) = Z.abs (signed x).

Lemma abs_overflow [m] (Hm : m mod 2 = 0)
  (x : Zmod m) (Hx : signed x = -m/2) : abs x = x.

Lemma signed_abs_nonneg_small [m] (x : Zmod m) (H : signed x <> - m / 2):
  0 <= signed (abs x).

Lemma signed_abs_nonneg_odd [m] (Hm : m mod 2 = 1) (x : Zmod m) :
  0 <= signed (abs x).

Lemma abs_mul_abs_l [m] (x y : Zmod m) : abs (abs x * y) = abs (x * y).

Lemma abs_mul_abs_r [m] (x y : Zmod m) : abs (x * abs y) = abs (x * y).

Lemma abs_mul_abs_abs [m] (x y : Zmod m) : abs (abs x * abs y) = abs (x * y).

Lemma gcd_opp_m [m] x : Z.gcd (@opp m x) m = Z.gcd x m.

Lemma gcd_abs_m_odd [m] (Hm : m mod 2 = 1) x :
  Z.gcd (@abs m x) m = Z.gcd x m.

Lemma pow_opp_2 [m] (x : Zmod m) : pow (opp x) 2 = pow x 2.

Lemma pow_abs_2 [m] (x : Zmod m) : pow (abs x) 2 = pow x 2.

Lemma eq_abs_iff m (x y : Zmod m) : abs x = abs y <-> (y = x \/ y = opp x).

Lemma length_elements m : length (elements m) = Z.abs_nat m.

Lemma nth_error_elements [m] n : List.nth_error (elements m) n =
  if (Nat.ltb n (Z.abs_nat m)) then Some (of_Z _ (Z.of_nat n)) else None.

Lemma in_elements [m] a (Hm : m <> 0) : List.In a (elements m).

Lemma NoDup_elements m : List.NoDup (elements m).

Example elements_0 : elements 0 = [].

Lemma elements_by_sign m (Hm : m <> 0) :
  elements m = [zero] ++ positives m ++ negatives m.

Lemma elements_by_sign' m :
  elements m = List.firstn (Z.abs_nat m) [zero] ++ positives m ++ negatives m.

Lemma in_positives m x (Hm : m <> 0) : In x (positives m) <-> 0 < signed x.

Lemma in_negatives m x (Hm : m <> 0) : In x (negatives m) <-> signed x < 0.

Lemma NoDup_positives m : NoDup (positives m).

Lemma NoDup_negatives m : NoDup (negatives m).

Lemma length_positives' m : length (positives m) = Z.to_nat ((Z.abs m - Z.b2z (0 <? m)) / 2).

Lemma length_positives m (Hm : 0 < m) : length (positives m) = Z.to_nat ((m-1)/2).

Lemma length_negatives m (Hm : 0 < m) : length (negatives m) = Z.to_nat (m/2).

Lemma negatives_as_positives_odd m (Hm : m mod 2 = 1) :
  negatives m = map opp (rev (positives m)).

Lemma invertibles_prime p (H : Z.prime p) :
  invertibles p = List.tl (elements p).

Lemma length_invertibles_prime p (H : Z.prime p) :
  length (invertibles p) = Z.to_nat (p-1).

End Zmod.