proposition: Lemma cnf_size_nz x (m:= cnf_size x): cnfp_nz x -> natp m /\ domain x = csucc m.
proof: Proof. move => [ox /domain_set0_P xnz]. exact: (cpred_pr (proj42 ox) xnz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)