proposition: Lemma Exercise1_20e: ~ (scattered cantor_tri_order).
proof: Proof. move=> ns. set (all_a := Zo cantor_tri_sub (fun z => exists2 i, natp i & forall j, natp j -> i <=c j -> Vg z j = C0)). set (F:= cantor_tri_sub -s all_a). have sF: (sub F cantor_tri_sub) by apply: sub_setC. have FpP: forall a, inc a F <-> (inc a cantor_tri_sub /\ forall i, natp i -> exists j, [/\ natp j, i <=c j & Vg a j = C1]). move=> a; split. move /setC_P => [p1 p2];split =>// i iN; ex_middle nf; case: p2. apply: Zo_i => //; exists i => // j jN ij; ex_middle vj; case: nf. exists j; split => //. move: p1 => /setXf_P [_ _ aux]; move: (aux _ jN);case/C2_P =>//. move => [pa pb]; apply /setC_P;split => //; move => /Zo_P [_ [i iN h]]. move: (pb _ iN) =>[j [p3 p4]];rewrite (h _ p3 p4); fprops. have sf1: sub F (substrate cantor_tri_order) by rewrite cantor_tri_order_sr. move: (iorder_osr (proj1 ns) sf1) => [xa xb]. move: ns => [oc ns]; case: (ns _ sf1);split; fprops. set zb:= (cst_graph Nat C1). set zab:= (Lg Nat (fun i => Yo (i = \0c) C0 C1)). have zbF: (inc zb F). apply /FpP; rewrite /zb; split. apply /setXf_P; split;aww => i iN; rewrite LgV; fprops. move=> i iN; exists i; split => //; fprops; rewrite LgV//. have zabF: inc zab F. apply /FpP; rewrite /zab; split. apply /setXf_P;split => //;aww => i iN; rewrite LgV//; Ytac h; fprops. move=> i iN; move:(NS_succ iN) => nsiN; exists (csucc i). split=> //; fprops; rewrite LgV// Y_false //; apply: succ_nz. have [lt1 ne1]: (glt cantor_tri_order zab zb). have zeb:= NS0. apply /cantor_tri_order_gltP => //;split => //. by move: zabF => /setC_P []. by move: zbF => /setC_P []. exists \0c; rewrite /zb /zab; split => //. + move => i iN iz; case: (clt0 iz). + by rewrite ! LgV//; Ytac0. + by rewrite LgV. exists zab, zb; split => //; apply /iorder_gleP => //. move=> f g fg. move: (iorder_gle2 fg)(iorder_gle4 fg). move /cantor_tri_order_gltP => [fsr gsr [j [jN sj fj gj]]][fs gs]. have scj:= NS_succ jN. move: (gs)=>/FpP [gc ha]. move: (ha _ scj) => [k [kN kle Vk]]. move: kle;rewrite cleSltP // => kle. set (h:= Lg Nat (fun i=> Yo (i= k) C0 (Vg g i))). have hF: inc h F. apply /FpP; split. rewrite /h;apply/setXf_P;split => //;aww=> i iN; rewrite LgV//; Ytac h0; fprops. by move: gc => /setXf_P [_ _]; apply. move=> i iN. move:(cmax_p1 (CS_nat iN) (CS_succ k)) => []; set l := cmax _ _ => sa sb. have lN: natp l by apply:Gmax_E => //; apply:NS_succ. move: (ha _ lN) => [n [nN mn Vb]]. exists n;split => //; first exact:(cleT sa mn). case: (equal_or_not k n) => kn; last by rewrite /h LgV//; Ytac0. by move:(cltS nN) (cleT sb mn); rewrite kn => sc /(cltNge sc). have [lt1 n1]: glt cantor_tri_order f h. apply /cantor_tri_order_gltP; split;fprops;exists j; split => //. move=> i iB ij; rewrite (sj _ iB ij); rewrite /h LgV//. by rewrite (Y_false (proj2 (clt_ltT ij kle))). by move: kle => [_ kne]; rewrite /h -gj LgV//; Ytac0. have [lt2 n2]: glt cantor_tri_order h g. apply /cantor_tri_order_gltP; split => //. by move: hF => /setC_P []. exists k; split => //; last by rewrite /h LgV//; Ytac0. by move=> i iB [_ iK]; rewrite /h LgV//; Ytac0. exists h; split => //; apply /iorder_gleP => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)