proposition: Lemma cnf_size_nz_ter x: cnfp_nz x -> inc \0c (domain x) /\ \0c <c domain x.
proof: Proof. move/cnf_size_nz =>[sN ->]; move:(succ_positive (cnf_size x)) => sp. by split => //; apply/(NltP (NS_succ sN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)