proposition: Lemma PN_prod a b: posnatp a -> posnatp b -> posnatp (a *c b).
proof: Proof. move => [aN /proj2/nesym az] [nN /proj2/nesym bz]. by apply:posnat_prop; fprops; apply: cprod2_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)