proposition: Lemma of_posnat_gt_0 : forall (p : posnat), 0 < N.of_nat p.
proof: Proof. intuition. unfold N.of_nat, posnatToNat. destruct p. destruct x. lia. destruct x; intuition; simpl in *. lia. lia. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat