proposition: Lemma CNFp_exists x: \0o <o x -> exists p n, [/\ CNFp_ax p n, natp n & x = CNFpv p n].
proof: Proof. move=> xp. move: (the_cnf_p0_nz xp) => [cp cv]. move:(proj44 (proj1 cp)). move: (cnf_size_nz cp); set n :=cnf_size _; move => [nN nv]; rewrite nv. move => ax. move: (CNFp_p3 ax nN) => [p [pa pb pc pd]]; exists p, n => //. by rewrite - cv - pb /cnf_val nv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)