proposition: Lemma mod_unique : forall b q1 r1 q2 r2, 0 <= r1 < b -> 0 <= r2 < b -> b * q1 + r1 = b * q2 + r2 -> q1 = q2 /\ r1 = r2.
proof: Proof. Proof with auto with zarith. intros b q1 r1 q2 r2 H1 H2 H3. assert (r2 = (b * q1 + r1) -b*q2). rewrite H3;ring. assert (b*(q2 - q1) = r1 - r2 ). rewrite H;ring. assert (-b < r1 - r2 < b). lia. destruct (Ztrichotomy q1 q2) as [H5 | [H5 | H5]]. assert (q2 - q1 >= 1). lia. assert (r1- r2 >= b). rewrite <- H0. pattern b at 2; replace b with (b*1). apply Zmult_ge_compat_l; lia. ring. exfalso; lia. split;trivial. rewrite H;rewrite H5;ring. assert (r1- r2 <= -b). rewrite <- H0. replace (-b) with (b*(-1)); try (ring;fail). apply Zmult_le_compat_l; lia. exfalso; lia. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod