proposition: Lemma ord_negl_p7_bis x y: \0o <o x -> \0o <o y -> (odegree x <o odegree y <-> x <<o y).
proof: Proof. move => xp yp; split; first by apply:ord_negl_p7. move:(the_cnf_p0_nz xp)(the_cnf_p0_nz yp). set a := the_cnf x; set b := the_cnf y. move => [anz av][bnz bv]. move: xp yp => [/proj32 ox /nesym xz][/proj32 oy /nesym yz] xy. move:(cnf_osum ox oy); rewrite xy -/a -/b => eq1. move: (odegree_sum ox oy); rewrite xy. case:(oleT_el (OS_degree oy) (OS_degree ox)) => // le1. rewrite (omax_yx le1) => dxdy. have sd: cnf_degree a = cnf_degree b. by move: dxdy; rewrite /odegree -/a -/b; Ytac0; Ytac0. move:(cnf_sd_lc anz bnz sd); rewrite - eq1. move:(posnat_lc anz)(posnat_lc bnz) =>[qa qb][qc qd] => eq2. by move:(proj2 (csum_M0lt qc (nesym(proj2 qb)))); rewrite csumC - eq2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)