proposition: Lemma posnat_add m n: natp m -> posnatp n -> posnatp (m +c n).
proof: Proof. move => mN [nN /proj2/nesym np];apply:(posnat_prop (NS_sum mN nN)). by case/csum_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)