proposition: Lemma cnf_lt_deg x y: cnfp_nz x -> cnfp_nz y -> cnf_degree x <o cnf_degree y -> x <f y.
proof: Proof. move => xp yp ltd. have H z e: cnfp z -> cnf_degree z <o e -> Vr z e = \0c. move => az h; rewrite /Vr Vg_out_of_range //. move => /funI_P [k /(range_gP (proj41 az)) [i idx ->] ev ]. by case: (oltNge h); move: (cnf_degree_greatest az idx); rewrite /oexp - ev. move: (proj1 xp)(proj1 yp) => ox oy. split; last by move => eq; case: (proj2 ltd); rewrite eq. split => //; right; exists (cnf_degree y). rewrite (H _ _ ox ltd) - (cnf_coef_of_lc yp). by case: (posnat_lc yp). by move => d dle; rewrite (H _ _ oy dle) (H _ _ ox (olt_ltT ltd dle)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)