proposition: Lemma modNat_correct_if : forall x y z (p : posnat), x * p + y = z -> modNat z p = modNat y p.
proof: Proof. induction x; intuition; simpl in *. subst. trivial. assert (x * p + (y + p) = z). lia. apply IHx in H0. rewrite H0. rewrite Nat.add_comm. rewrite modNat_plus. rewrite modNat_arg_eq. rewrite Nat.add_0_l. trivial. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat