proposition: Lemma NS_sum a b: natp a -> natp b -> natp (a +c b).
proof: Proof. move=> aN bN. move: b bN; apply: Nat_induction; first by rewrite Nsum0r. move=> n fn fan; rewrite (csum_nS a fn); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)