Library Stdlib.ZArith.Zcong

From Stdlib Require Import BinInt.
From Stdlib Require Import ZArithRing.
From Stdlib Require Import Zdiv.
From Stdlib Require Import Zdivisibility.
Local Open Scope Z_scope.

Module Z.

Lemma cong_mul_cancel_r_coprime a b m (Hm : m <> 0) (Hb : Z.coprime b m)
  (H : (a * b) mod m = 0) : a mod m = 0.

Definition invmod a m := fst (fst (Z.extgcd (a mod m) m)) mod m.

Lemma invmod_0_l m : invmod 0 m = 0.

Lemma invmod_0_r a : invmod a 0 = Z.sgn a.

Lemma invmod_ok a m : invmod a m * a mod m = Z.gcd a m mod m.

Lemma mod_invmod m a : invmod a m mod m = invmod a m.

Lemma invmod_coprime' a m (H : Z.coprime a m) : invmod a m * a mod m = 1 mod m.

Lemma invmod_coprime a m (Hm : 2 <= m) (H : Z.coprime a m) : invmod a m * a mod m = 1.

Lemma invmod_prime a m (Hm : Z.prime m) (H : a mod m <> 0) : invmod a m * a mod m = 1.

Lemma invmod_1_l m : invmod 1 m = 1 mod m.

Lemma invmod_mod_l a m : invmod (a mod m) m = invmod a m.

Lemma coprime_invmod a m (H : Z.coprime a m) : Z.coprime (invmod a m) m.

Definition combinecong (m1 m2 r1 r2 : Z) :=
  let '(u, v, d) := Z.extgcd m1 m2 in
  if Z.eq_dec (r1 mod d) (r2 mod d) then
    if Z.eq_dec d 0
    then r1
    else (v*m2*r1 + u*m1*r2) / d mod Z.abs (m1*(m2/d))
  else 0.

Lemma mod_combinecong_lcm m1 m2 r1 r2 :
  combinecong m1 m2 r1 r2 mod Z.lcm m1 m2 = combinecong m1 m2 r1 r2.

Lemma combinecong_sound m1 m2 r1 r2 (H : r1 mod Z.gcd m1 m2 = r2 mod Z.gcd m1 m2)
  (x := combinecong m1 m2 r1 r2) : x mod m1 = r1 mod m1 /\ x mod m2 = r2 mod m2.
Lemma combinecong_complete' a m1 m2 r1 r2
  (H1 : a mod m1 = r1 mod m1) (H2 : a mod m2 = r2 mod m2) :
  r1 mod Z.gcd m1 m2 = r2 mod Z.gcd m1 m2.

Lemma combinecong_complete a m1 m2 r1 r2
  (H1 : a mod m1 = r1 mod m1) (H2 : a mod m2 = r2 mod m2) :
  a mod Z.lcm m1 m2 = combinecong m1 m2 r1 r2.

Lemma combinecong_contradiction m1 m2 r1 r2 :
  r1 mod Z.gcd m1 m2 <> r2 mod Z.gcd m1 m2 -> combinecong m1 m2 r1 r2 = 0.

Lemma combinecong_sound_coprime m1 m2 r1 r2 (H : Z.coprime m1 m2)
  (x := combinecong m1 m2 r1 r2) : x mod m1 = r1 mod m1 /\ x mod m2 = r2 mod m2.

Lemma combinecong_complete_coprime_abs a m1 m2 r1 r2 (H : Z.coprime m1 m2)
  (H1 : a mod m1 = r1 mod m1) (H2 : a mod m2 = r2 mod m2) :
  a mod Z.abs (m1 * m2) = combinecong m1 m2 r1 r2.

Lemma combinecong_complete_coprime_nonneg a m1 m2 r1 r2 (H : Z.coprime m1 m2)
  (H1 : a mod m1 = r1 mod m1) (H2 : a mod m2 = r2 mod m2) (Hm : 0 <= m1*m2) :
  a mod (m1 * m2) = combinecong m1 m2 r1 r2.

Lemma combinecong_complete_coprime_nonneg_nonneg a m1 m2 r1 r2 (H : Z.coprime m1 m2)
  (H1 : a mod m1 = r1 mod m1) (H2 : a mod m2 = r2 mod m2) (Hm1 : 0 <= m1) (Hm2 : 0 <= m2) :
  a mod (m1 * m2) = combinecong m1 m2 r1 r2.

Lemma combinecong_comm m1 m2 r1 r2 :
  combinecong m1 m2 r1 r2 = combinecong m2 m1 r2 r1.

Lemma combinecong_mod_l m1 m2 r1 r2 :
  combinecong m1 m2 (r1 mod m1) r2 = combinecong m1 m2 r1 r2.

Lemma combinecong_mod_r m1 m2 r1 r2 :
  combinecong m1 m2 r1 (r2 mod m2) = combinecong m1 m2 r1 r2.

Lemma combinecong_opp_opp (m1 m2 r1 r2 : Z) :
  combinecong m1 m2 (- r1) (- r2) = - combinecong m1 m2 r1 r2 mod Z.lcm m1 m2.
End Z.