proposition: Lemma cnf_degree_greatest x i: cnfp x -> inc i (domain x) -> oexp x i <=o cnf_degree x.
proof: Proof. move => ox; move: (proj42 ox) => dN /(NltP dN) lidx. case: (equal_or_not x emptyset) => xe. by move: lidx; rewrite xe domain_set0 => /clt0. move:(cnf_size_nz (conj ox xe)) => [mN mv]. move: lidx; rewrite mv => /(cltSleP mN) => /cle_eqVlt; case. by move ->; apply: oleR; apply: OS_cnf_degree. by move/(cnf_degree_greatest_bis ox); case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)