proposition: Lemma modNat_lt : forall x p, (modNat x p < p)%nat.
proof: Proof. intuition. unfold modNat. assert (N.of_nat x mod N.of_nat p < N.of_nat p)%N. apply N.mod_bound_pos. apply of_nat_ge_0. apply of_posnat_gt_0. specialize (Nnat.N2Nat.inj_compare); intros H0. rewrite <- (Nnat.Nat2N.id p) at 2. apply nat_compare_lt. rewrite <- H0. apply N.compare_lt_iff. trivial. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat