proposition: Lemma modNat_add_same_r : forall x y z p, modNat (y + x) p = modNat (z + x) p -> modNat y p = modNat z p.
proof: Proof. intuition. eapply (modNat_add_same_l x y z). rewrite Nat.add_comm. rewrite H. rewrite Nat.add_comm. trivial. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat