proposition: Lemma uniqueRem : forall r1 r2 b : nat, b > 0 -> forall a : nat, (exists q : nat, a = q * b + r1 /\ b > r1) -> (exists q : nat, a = q * b + r2 /\ b > r2) -> r1 = r2.
proof: Proof. intros ? ? ? H a [x [H0 H2]] [x0 [H1 H3]]. assert (x = x0). { nia. } nia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow