proposition: Lemma modNat_add_same_l : forall x y z p, modNat (x + y) p = modNat (x + z) p -> modNat y p = modNat z p.
proof: Proof. induction x; intuition; simpl in *. assert (S (x + y) = x + S y). lia. rewrite H0 in H. clear H0. assert (S (x + z) = x + S z). lia. rewrite H0 in H. clear H0. apply IHx in H. destruct (modNat_correct (S y) p). destruct (modNat_correct (S z) p). rewrite H in H0. assert (S y - x0 * p = modNat (S z) p). lia. assert (S z - x1 * p = modNat (S z) p). lia. rewrite <- H2 in H3. assert (z - x1 * p = y - x0 * p). lia. assert (x1 * p + y = x0 * p + z). lia. apply modNat_correct_if in H5. rewrite modNat_plus in H5. rewrite modNat_mult in H5. rewrite Nat.add_0_l in H5. auto. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat