proposition: Lemma modNat_correct : forall x (p : posnat), exists k, (x = k * p + modNat x p)%nat.
proof: Proof. intuition. unfold modNat in *. assert (p > 0)%nat. eapply posnat_pos. assert (posnatToNat p <> 0)%nat. lia. assert (N.of_nat p <> 0%N). intro. eapply H0. rewrite <- Nnat.Nat2N.id. rewrite <- (Nnat.Nat2N.id p). f_equal. trivial. exists (N.to_nat (N.of_nat x / N.of_nat p)). rewrite N.mod_eq; trivial. rewrite <- (Nnat.Nat2N.id p) at 2. rewrite <- Nnat.N2Nat.inj_mul. rewrite <- Nnat.N2Nat.inj_add. rewrite N.mul_comm. remember (N.of_nat p * (N.of_nat x / N.of_nat p)) as z. rewrite N.add_sub_assoc. rewrite N.add_comm. rewrite N.add_sub. rewrite Nnat.Nat2N.id. trivial. subst. eapply N.mul_div_le. trivial. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat