proposition: Lemma cnf_subset_prop E c x: finite_set E -> natp c -> inc x (cnf_subset E c) -> [/\ cnfp x, sub (cnf_exponents x) E & forall e, Vr x e <=c c].
proof: Proof. move => rF cN /funI_P [z /Zo_P [/setP_P qa qb] xv ]. move: (cnf_sort_correct qb); rewrite - xv; move =>[qc qd]; split. - exact. - by rewrite /cnf_exponents qd => t/funI_P [k /qa /setX_P [_ h _] -> ]. - move => e; case: (inc_or_not e (cnf_exponents x)) => eE. move: eE => /funI_P [k ka ->]; rewrite (Vr_in_range qc ka). by move: ka; rewrite /cnf_exponents qd => /qa /setX_P [_ _ q];apply /NleP. by rewrite (Vr_oor eE);apply: cle0n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)