proposition: Lemma cnf_nck_prop3 x k: cnfp_nz x -> natp k -> cnfp (cnf_nck x (csucc k)).
proof: Proof. move => xnz kN. rewrite (cnf_nck_prop1 _ kN). move:(NS_prod (proj1 (posnat_lc xnz)) kN) => aux. by case:(cnf_nc_prop xnz aux). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)