proposition: Lemma BZsum_N_Ns x y: natp x -> inc y Nats -> inc (x +c y) Nats.
proof: Proof. move => xb /setC1_P [yn yz]; apply /setC1_P;split; first by apply: NS_sum. move: (cpred_pr yn yz) => [pa pb]. rewrite pb (csum_nS _ pa);apply: succ_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)