proposition: Lemma Exercise1_21n r x: total_order r -> inc x (substrate r) -> scattered (induced_order r (class (scattered_equiv r) x)).
proof: Proof. move=> tor xsr. move: (Exercise1_21i tor)(Exercise1_21j tor) => es ss. move: tor => [or tor]. have sc:(sub (class (scattered_equiv r) x) (substrate r)). by rewrite - ss;apply: sub_class_substrate. move: (iorder_osr or sc) => [pa pb]. split => //. move=> y; rewrite iorder_sr // => yc; rewrite (iorder_trans _ yc). have yp: forall u, inc u y -> related (scattered_equiv r) u x. move=> u uy; move: (yc _ uy) => /(class_P es) aux; equiv_tac. move=>[oiy [a [b rab]] wg2]. move: (iorder_gle4 rab)=> [ay biy]; move: (yp _ ay) (yp _ biy)=> ax bx. have xb:(related (scattered_equiv r) x b) by equiv_tac. have :(related (scattered_equiv r) a b ) by equiv_tac. apply /Exercise1_21l =>//; case; move=> [aux1 aux2]; last first. move: (iorder_gle2 rab) => aux3; order_tac. have asr: inc a (substrate r) by order_tac. have bsr: inc b (substrate r) by order_tac. move: (@subsetI2r y (interval_cc r a b)) => uy. case: (aux2 _ uy). set u:= _ \cap _. have au:inc a u by apply: setI2_i => //;apply:Zo_i => //;split =>//;order_tac. have bu:inc b u by apply: setI2_i => //;apply:Zo_i => //;split =>//;order_tac. by move=> aux3; move: (aux3 _ _ au bu); case: rab. move=> [c [d [cu du cd cde]]]. have cd1: (glt (induced_order r y) c d). apply /iorder_gltP;split => //; [ apply:(setI2_1 cu) |apply: (setI2_1 du) ]. move: (wg2 _ _ cd1) => [e ce ed]. move:(iorder_gle4 ce)(iorder_gle2 ce) (iorder_gle2 ed) => [_ er] ce' de'. have aux:inc e (y \cap (interval_cc r a b)). apply: setI2_i => //; apply: Zo_i; [ order_tac | split => //]. move:(setI2_2 cu) => /Zo_hi [ac _]. move: ce' => [ce' _];order_tac. move:(setI2_2 du) => /Zo_hi [_ db]. move: de' => [de' _];order_tac. case: (cde _ aux)=> aux3; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)