proposition: Lemma modNatAddInverse_correct_gen : forall x y p, modNat x p = modNat y p -> modNat (x + modNatAddInverse y p) p = O.
proof: Proof. intuition. unfold modNatAddInverse. rewrite <- H. rewrite modNat_plus. rewrite minus_add_assoc. rewrite (Nat.add_comm). rewrite <- minus_add_assoc. rewrite Nat.sub_diag. rewrite Nat.add_0_r. apply modNat_arg_eq. trivial. assert (modNat x p < p)%nat. apply modNat_lt. lia. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat