proposition: Lemma cnf_le_total x y: cnfp x -> cnfp y -> x <=f y \/ y <=f x.
proof: Proof. move => ox oy. set F :=Vr. case:(p_or_not_p (exists e, F x e <> F y e)); last first. move => bad; left; split => //; left. by apply:(Vr_exten ox oy) => e; ex_middle w; case: bad; exists e. set E := (cnf_exponents x \cup cnf_exponents y). have ha e: F x e <> F y e -> inc e E. move => ep;rewrite /E;case: (equal_or_not (F x e) \0o) => fz. move/nesym: ep; rewrite fz => /Vr_ne; fprops. move/Vr_ne: fz; fprops. move => [e0 e0p]. set Ep := Zo E (fun e => F x e <> F y e). have hb e: F x e <> F y e -> inc e Ep by move => he;apply:Zo_i => //; apply:ha. move: (cnf_exponents_of oy); move => [ qa qb]. move: (cnf_exponents_of ox); move => [ qc qd]. have neF: nonempty Ep by exists e0; apply: hb. have fsF: finite_set Ep. by apply:sub_finite_set (setU2_finite qc qa); apply: Zo_S. have osF: ordinal_set Ep by move => t /Zo_S /setU2_P;case; fprops. move:(finite_subset_ord fsF neF osF)=> [e1 /Zo_P[e1E el1] aux]. have e1l e: e1 <o e -> F x e = F y e. move => lt1; ex_middle bad. have ee: inc e Ep by apply: hb. by case : (oleNgt (aux _ ee)). clear qa qb qc qd neF fsF aux. case: (NleT_ell (NS_Vr e1 ox) (NS_Vr e1 oy))=> cp. - by case el1. - by left; split => //; right; exists e1 => //. - by right; split => //; right; exists e1 => // i /e1l //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)