proposition: Lemma modNat_eq : forall (n : posnat) x, (x < n -> modNat x n = x)%nat.
proof: Proof. intuition. unfold modNat. rewrite N.mod_small. apply Nnat.Nat2N.id. specialize (Nnat.N2Nat.inj_compare); intuition. specialize (N.compare_lt_iff (N.of_nat x) (N.of_nat n)); intuition. apply H2. rewrite H0. repeat rewrite Nnat.Nat2N.id. apply nat_compare_lt. trivial. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat