proposition: Lemma cnf_le_compat x y: cnfp x -> cnfp y -> ( x <=f y <-> cnf_val x <=o cnf_val y).
proof: Proof. move => ox oy. pose R := fun x y => x <=f y <-> cnf_val x <=o cnf_val y. have R0y z: cnfp z -> R emptyset z. move => oz;rewrite /R cnf_val0; split => _. by apply: ole0x; apply:OS_cnf_val. by apply: cnf_le0x. have Rx0 z: cnfp z -> R z emptyset. move => oz;rewrite /R cnf_val0; split => h. move/cnf_lex0:h ->; rewrite cnf_val0; apply: (oleR OS0). case: (equal_or_not z emptyset) => znz. rewrite - znz; apply: (cnf_leR oz). by case(oltNge (OS_cnf_valp (conj oz znz))). pose deg z := Yo (z = emptyset) \0o (cnf_degree z). have od1 z: cnfp z -> ordinalp (deg z). by move => oe; rewrite /deg; Ytac h; fprops; apply: OS_cnf_degree. move:(od1 _ ox) (od1 _ oy) => qa qb. case: (omax_p1 qa qb). have: ordinalp (omax (deg x) (deg y)) by rewrite /omax/Gmax; Ytac hh. move: (omax _ _); clear qa qb => d od. move: d od x y ox oy. apply: least_ordinal2 => d od Hrec x y ox oy lt1 lt2. wlog: x y ox oy lt1 lt2 / deg x <=o deg y. move => hh; case: (oleT_ee (proj31 lt1) (proj31 lt2)); first by apply: hh. move => lt3; move: (hh y x oy ox lt2 lt1 lt3) => aux. move: (OS_cnf_val ox) (OS_cnf_val oy) => oa ob. case: (equal_or_not x y) => exy. rewrite - exy; split => _; [ apply: (oleR oa) | apply: (cnf_leR ox)]. split => lt5. by case: (oleT_ee oa ob);[ | move/aux => h; case: exy; apply: cnf_leA]. case: (cnf_le_total ox oy) => // /aux h; case: exy; move: (oleA lt5 h). by move/(cnf_val_inj ox oy). move => ledxdy. case: (equal_or_not x emptyset) => xnz; first by rewrite xnz; apply:R0y. case: (equal_or_not y emptyset) => ynz; first by rewrite ynz; apply:Rx0. case: (ole_eqVlt lt2) => lt2'; last first. apply: (Hrec _ lt2' _ _ ox oy ledxdy (oleR (proj31 lt2))). have yp: cnfp_nz y by []. have dyv: cnf_degree y = d by rewrite -lt2' /deg; Ytac0. move :(cnf_sum_prop5 yp); rewrite dyv => eq1. move:(cnf_rem_prop1 oy) (OS_cnf_rem oy) => ryv ory. move: (posnat_lc yp) => lcyp. have lt3: cnf_degree x <=o d. by move: ledxdy; rewrite lt2' /deg; Ytac0. move: (OS_oopow (proj32 lt3)) => ood. have xp: cnfp_nz x by split. move: (cnf_size_nz xp) (cnf_size_nz yp)=> [nN sxv] [mN syv]. move: (ox) (oy) => [ox1 ox2 ox3 ox4] [oy1 oy2 oy3 oy4]. case: (ole_eqVlt lt3) => cxy; last first. split => _; last first. rewrite - dyv in cxy. exact: (proj1 (cnf_lt_deg (conj ox xnz) (conj oy ynz) cxy)). move: ox4; rewrite eq1 /cnf_val sxv => axx. move /posnat_ordinalp: lcyp => [qa qb]. apply(oleT (proj1 (CNFq_pg2 nN (proj1 axx) cxy))). apply: (oleT (oprod_Mle1 ood qa)). apply: (osum_Mle0 (OS_prod2 ood (proj32_1 qa)) ory). move :(cnf_sum_prop5 xp); rewrite cxy => eq2. move:(cnf_rem_prop1 ox) (OS_cnf_rem ox) => rxv orx. move: (posnat_lc xp) => lcxp. move: (cnf_and_val_pb oy) =>[_ ovy eqa _]. have cyp: \0o <o (cnf_val y) by apply: OS_cnf_valp. move: (proj43 (the_cnf_split cyp)). rewrite /the_cnf_rem /odegree eqa (Y_false (nesym (proj2 cyp))) dyv => rys. move: (cnf_and_val_pb ox) =>[_ ovx eqb _]. have cxp: \0o <o (cnf_val x) by apply: OS_cnf_valp. move: (proj43 (the_cnf_split cxp)). rewrite /the_cnf_rem /odegree eqb (Y_false (nesym (proj2 cxp))) cxy => rxs. have sd: cnf_degree x = cnf_degree y by rewrite cxy. move:(OS_nat(proj1 lcxp)) (OS_nat (proj1 lcyp)) => olcx olcy. move:(OS_prod2 ood olcx)(OS_prod2 ood olcy) => ofx ofy. have ca: cnf_lc y <c cnf_lc x -> R x y. move => clc;split => h. by move: (cnf_lt_eq_deg yp xp (esym sd) clc)=> [qa]; case; apply: cnf_leA. have h': osucc (cnf_lc y) <=o cnf_lc x by apply/oleSltP; apply: oclt. have la: oopow d *o cnf_lc x <=o cnf_val x. rewrite eq2; apply: (osum_Mle0 ofx orx). have lb: cnf_val y <o oopow d *o (osucc (cnf_lc y)). rewrite eq1 (oprod2_succ ood olcy); apply: (osum_Meqlt rys ofy). by case: (oltNge (olt_leT lb (oleT (oprod_Meqle h' ood) la)) h). have cb: cnf_lc x <c cnf_lc y -> R x y. move => clc;split => _; last exact: (proj1 (cnf_lt_eq_deg xp yp sd clc)). have h': osucc (cnf_lc x) <=o cnf_lc y by apply/oleSltP; apply: oclt. have la: oopow d *o cnf_lc y <=o cnf_val y. rewrite eq1; apply: (osum_Mle0 ofy ory). have lb: cnf_val x <o oopow d *o (osucc (cnf_lc x)). rewrite eq2 (oprod2_succ ood olcx); apply: (osum_Meqlt rxs ofx). exact: (oleT (oleT (proj1 lb) (oprod_Meqle h' ood)) la). case: (NleT_ell (proj1 lcxp) (proj1 lcyp)); [ | exact | exact ]. move => slc; clear ca cb. set x' := (cnf_nr x (cnf_size x)). set y' := (cnf_nr y (cnf_size y)). have qa: (cnf_size x) <c (domain x) by rewrite sxv; apply : cltS. have qb: (cnf_size y) <c (domain y) by rewrite syv; apply : cltS. move: (cnfp_cnf_nr ox (proj1 qa)) (cnfp_cnf_nr oy (proj1 qb)) => rb rc. have rg: cnf_val x' <=o cnf_val y' <-> cnf_val x <=o cnf_val y. rewrite eq1 eq2 /x' /y' - rxv - ryv - slc; split => ll. by apply:(osum_Meqle ll ofx). by apply: (osum_Meqler orx ory ofx). apply: iff_trans rg. clear ofx ofy rxs rys eqa eqb eq1 eq2 rxv ryv cxp cyp ovx ovy. have dx': domain x' = cnf_size x by rewrite /x'/cnf_nr; aw. have dy': domain y' = cnf_size y by rewrite /y'/cnf_nr; aw. have cxy2 z: cnfp z -> z <> emptyset -> Vr (cnf_nr z (cnf_size z)) (cnf_degree z) = \0c /\ forall e, e <> (cnf_degree z) -> Vr (cnf_nr z (cnf_size z)) e = Vr z e. set z' := cnf_nr z (cnf_size z). move => oz znz. move: (cnf_size_nz (conj oz znz)) => [nN' szv]. have qe: (cnf_size z) <c (domain z) by rewrite szv; apply : cltS. move: (cnfp_cnf_nr oz (proj1 qe)) => oz'. split. rewrite /Vr Vg_out_of_range // => /funI_P [t tr tv]. move/(range_gP (proj41 oz')): tr; rewrite /cnf_nr; aw. move => [i idx ]; rewrite LgV // => xx. move/(NltP nN'): idx => ilx. move/(NltP (proj42 oz)): (clt_ltT ilx qe) => idz. move/(NltP (proj42 oz)): qe => qz'. have eq: oexp z (cnf_size z) = oexp z i by rewrite /oexp -xx. by case: (proj2 ilx);move: (cnf_monomial_inj oz qz' idz eq). move => e bed. case: (inc_or_not e (domain (range z'))) => er. move: er => /funI_P [t /(range_gP (proj41 oz')) [i idz ->] -> ]. rewrite (Vr_correct oz' idz). move: idz; rewrite /cnf_nr restr_d /ocoef => idz; rewrite LgV//. rewrite -/(ocoef z i)- (Vr_correct) //. by apply/(NltP (proj42 oz)); apply: clt_ltT qe; apply/NltP. rewrite /Vr (Vg_out_of_range er) Vg_out_of_range //. move /funI_P => [t /(range_gP (proj41 oz)) [i idz iv] tv ]. move/(NltP (proj42 oz)): idz; rewrite szv; move/(cltSleP nN'). case/cle_eqVlt; first by move => h; case: bed; rewrite tv iv h. move/(NltP nN') => idz. case: er; apply/funI_P; exists t => //; apply /(range_gP (proj41 oz')). aw; ex_tac; rewrite /cnf_nr LgV//. have rh: x <=f y <-> x' <=f y'. have qc: inc (cnf_size x) (domain x) by apply/(NltP ox2). have qd: inc (cnf_size y) (domain y) by apply/(NltP oy2). have slm: Vg x (cnf_size x) = Vg y (cnf_size y). by apply: (pair_exten (ox3 _ qc) (oy3 _ qd)). have H a b: a <c b -> b <> \0c. move => h; exact: (nesym (proj2 (cle_ltT (cle0x (proj31_1 h)) h))). have cx1:= (cnf_coef_of_lc (conj ox xnz)). have cy1:= (cnf_coef_of_lc (conj oy ynz)). move: (cxy2 _ ox xnz) (cxy2 _ oy ynz); rewrite -/x' -/y'. move=> [cx2 cx3] [cy2 cy3] . clear cxy2. split; move => [_ _ lrp]; split; [exact | exact | | exact | exact | ]. case: lrp; first by rewrite /x'/y' ; move ->; left. move => [e ea eb]; right. exists e. move: ea; case:(equal_or_not e (cnf_degree x))=> h. by case/proj2; rewrite h - cx1 sd - cy1. by rewrite (cx3 e h) cy3 // - sd. move => j lee; move: (eb _ lee); case:(equal_or_not j (cnf_degree x))=> h. by rewrite h cx2 sd cy2. by rewrite (cx3 j h) cy3 // - sd. case: lrp => sv. have dd1: cnf_size x = cnf_size y by rewrite - dx' - dy' sv. have dd: domain x = domain y by rewrite sxv syv dd1. left; apply:(fgraph_exten ox1 oy1 dd) => i /(NltP ox2). rewrite sxv => /(cltSleP nN); case/cle_eqVlt. by move ->;rewrite {2} dd1. move/(NltP nN)=> id1. by move: (f_equal (Vg ^~i) sv); rewrite /x'/y'/cnf_nr !LgV // - dd1. move:sv => [e ea eb]; right. exists e. move: ea; case:(equal_or_not e (cnf_degree x))=> h. by case/proj2; rewrite h cx2 sd - cy2. by rewrite (cx3 e h) cy3 // - sd. move => j lee; move: (eb _ lee); case:(equal_or_not j (cnf_degree x))=> h. by move => _; rewrite h - cx1 sd - cy1. by rewrite (cx3 j h) cy3 // - sd. apply:(iff_trans rh). case: (equal_or_not x' emptyset) => xnz'; first by rewrite xnz'; apply:R0y. case: (equal_or_not y' emptyset) => ynz'; first by rewrite ynz'; apply:Rx0. have dx1 : deg x' <o d. rewrite /deg - cxy; Ytac0; rewrite /cnf_degree /oexp /x' /cnf_size restr_d. case: (equal_or_not (cnf_size x) \0c) => sz. by case: xnz'; apply/domain_set0_P; rewrite dx'. move: (cpred_pr nN sz) => [qN qv]. have qe: inc (cpred (cnf_size x)) (cnf_size x). by rewrite {2} qv; apply:Nsucc_i. rewrite sxv (cpred_pr1 (CS_nat nN)) LgV//. by move: (proj44 (proj1 (proj44 ox)) _ qN); rewrite - qv; apply. have dy1 : deg y' <o d. rewrite /deg - dyv; Ytac0; rewrite /cnf_degree /oexp /y' /cnf_size restr_d. case: (equal_or_not (cnf_size y) \0c) => sz. by case: ynz'; apply/domain_set0_P; rewrite dy'. move: (cpred_pr mN sz) => [qN qv]. have qe: inc (cpred (cnf_size y)) (cnf_size y). by rewrite {2} qv; apply:Nsucc_i. rewrite syv (cpred_pr1 (CS_nat mN)) LgV//. by move: (proj44 (proj1 (proj44 oy)) _ qN); rewrite - qv; apply. set d' := omax (deg x') (deg y'). have lta: d' <o d by rewrite /d'/omax/Gmax; Ytac w. move: (omax_p1 (proj31_1 dx1) (proj31_1 dy1)) => [sa sb]. exact: (Hrec _ lta _ _ rb rc sa sb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)