proposition: Lemma modNatAddInverse_sum_0 : forall x y p, modNat (x + (modNatAddInverse y p)) p = O -> modNat x p = modNat y p.
proof: Proof. intuition. assert (modNat x p < p). eapply modNat_lt. assert (modNat y p < p). eapply modNat_lt. rewrite modNat_plus in H. unfold modNatAddInverse in *. rewrite minus_add_assoc in H; intuition. rewrite Nat.add_comm in H. apply modNat_divides in H. destruct H. remember (modNat x p) as a. remember (modNat y p) as b. assert (p + a >= p). lia. assert (p + a < 2 * p)%nat. lia. assert (p + a - b < 2 * p). lia. assert (p + a - b > 0). lia. assert (x0 * p > 0). lia. assert (x0 * p < 2 * p). lia. destruct x0. lia. destruct x0. simpl in H. rewrite Nat.add_0_r in H. lia. assert (p > 0). eapply posnat_pos. simpl in H7. remember (x0 * p)%nat as c. lia. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat