proposition: Lemma cnf_all_smaller_prop x y: cnfp x -> cnfp y -> [\/ x = emptyset, y = emptyset | (cnf_degree x) <o (oexp y \0c) ] -> cnf_all_smaller x y.
proof: Proof. rewrite/cnf_all_smaller;move => ox oy; case. - by move ->; rewrite domain_set0 => i j /clt0. - by move ->; rewrite domain_set0 => i j _ /clt0. - move => h1 i j /(NltP (proj42 ox)) idx jdy. apply: (olt_leT (ole_ltT (cnf_degree_greatest ox idx) h1)). apply: (CNF_exponents_M (proj42 oy) (proj1 (proj44 oy)) _ jdy). exact:(cle0x (proj31_1 jdy)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)