proposition: Lemma cnf_degree_greatest_bis x i: cnfp x -> i <c (cnf_size x) -> oexp x i <o cnf_degree x.
proof: Proof. move => ox lt1; apply: (CNF_exponents_sM (proj42 ox) (proj1 (proj44 ox)) lt1). have aux:cnfp_nz x. split => //xe. by move:lt1; rewrite xe /cnf_size domain_set0 cpred0 => /clt0. apply/(NltP (proj42 ox)); apply:(cnf_size_nz_bis aux). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)