proposition: Lemma modNat_arg_eq : forall (p : posnat), modNat p p = O.
proof: Proof. intuition. unfold modNat. rewrite N.mod_same. trivial. unfold N.of_nat, posnatToNat. destruct p. destruct x. lia. apply Npos_nz. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat