proposition: Lemma Exercise1_20d: Exercise1_20_prop cantor_tri_order.
proof: Proof. move=> x y. move /cantor_tri_order_gltP => [xb yb [j [jN sj jx jy]]]. pose f i := Yo (i <=c j) (Vg x i) C1. pose g i := Yo (i <=c j) (Vg y i) C0. have fgPr: (fgraph (cst_graph Nat C2)) by fprops. move: (xb)(yb) => /setXf_P [fgx dx xVV] /setXf_P [fgy dy yVV]. have fPr: (inc (Lg Nat f) cantor_tri_sub). apply /setXf_P;split;aww;move=> i iN; rewrite /f LgV//. Ytac hle; fprops. have gPr: (inc (Lg Nat g) cantor_tri_sub ). apply /setXf_P;split;aww;move=> i iN; rewrite /g LgV//. Ytac h; fprops. move: cantor_tri_order_total => [co _]. pose Zab a x := Zo Nat (fun i => j <c i /\ Vg x i = a). have Zabp: forall a x, nonempty (Zab a x) -> exists k, [/\ natp k, j <c k, Vg x k = a & (forall i, natp i -> i <c k -> i <=c j \/ Vg x i <> a)]. move=> a u [v vZ]. have ov: ordinalp v by apply /OS_nat; apply: (Zo_S vZ). move: (least_ordinal4 (p := fun z=> inc z (Zab a u)) ov vZ). set w:= least_ordinal _ _ ; move => [wa /Zo_P [wb [wc wd]] we]. exists w; split => // i iN iw; case: (inc_or_not i (Zab a u)) => h. case: (oleNgt (we _ (OS_nat iN) h) (oclt iw)). case: (equal_or_not (Vg u i) a) => eq; last by right. by case: (NleT_el iN (NS_lt_nat wc wb))=> ji; [by left | case: h;apply: Zo_i]. have p1: gle cantor_tri_order x (Lg Nat f). case: (emptyset_dichot (Zab C0 x)) => Ze. suff: x = (Lg Nat f) by move=> <- ;order_tac;rewrite cantor_tri_order_sr. apply: fgraph_exten => //; aww. rewrite dx; move=> i iN; rewrite /f LgV//. Ytac hle =>//; move: (xVV _ iN); aw; case/C2_P => // vb. by empty_tac1 i; apply: Zo_i => //; split => //;case: (NleT_el iN jN). suff: glt cantor_tri_order x (Lg Nat f) by case. move:(Zabp C0 x Ze) => [k [kN jk vk lt]]. apply /cantor_tri_order_gltP; split => //. exists k; split => //; last by rewrite LgV// /f (Y_false (cltNge jk)). move=> i iN ik; rewrite /f LgV//. Ytac hle => //; case: (lt _ iN ik)=> // va. move: (xVV _ iN);aw; case/C2_P => //. have p2: gle cantor_tri_order (Lg Nat g) y. case: (emptyset_dichot (Zab C1 y)) => Ze. suff: y = (Lg Nat g) by move=> <- ;order_tac;rewrite cantor_tri_order_sr //. apply: fgraph_exten => //; aww. rewrite dy; move=> i iN; rewrite /g LgV//. Ytac hle => //; move: (yVV _ iN); case/C2_P => // vb. by empty_tac1 i; apply: Zo_i => //;split => //; case: (NleT_el iN jN). suff: glt cantor_tri_order (Lg Nat g) y by case. move:(Zabp C1 y Ze) => [k [kN jk vk lt]]. apply /cantor_tri_order_gltP; split => //. exists k; split => //; last by rewrite /g LgV// (Y_false (cltNge jk)). move=> i iN ik; rewrite /g LgV//; Ytac ij => //. case: (lt _ iN ik)=> // va; move: (yVV _ iN); case/C2_P=> //. have jj: j <=c j by apply: cleR; fprops. exists (Lg Nat f), (Lg Nat g); split => //. apply /cantor_tri_order_gltP;split => //;exists j. rewrite /f/g!LgV//; Ytac0; Ytac0; split => //. by move => i ib [ij nij]; rewrite !LgV//; Ytac0; Ytac0;apply: sj. move=> z [] /cantor_tri_order_gltP [_ zsub [k1 [k1N k1p k1a k1b]]]. move /cantor_tri_order_gltP => [_ _ [k2 [k2N k2p k2a k2b]]]. move: k1a k2b; rewrite /f /g ! LgV//; Ytac k1j; Ytac k2j => k1a k2b; try (solve [apply: C0_ne_C1; done]). case: (NleT_el k1N k2N) => k1k2. have l12: k1 <c k2 by split =>//h; case: C0_ne_C1; rewrite -k1b -k2a h. move: (k2p _ k1N l12); rewrite /g LgV// (Y_true k1j) k1b. rewrite -(sj _ k1N (clt_leT l12 k2j)) k1a; fprops. move: (k1p _ k2N k1k2); rewrite /f LgV// (Y_true k2j) k2a. rewrite (sj _ k2N (clt_leT k1k2 k1j)) k2b; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)