proposition: Lemma Exercise1_21h r: total_order r -> equivalence_re (scattered_rel r) (substrate r).
proof: Proof. move=> tor; move: (tor) => [or tor']. have Ha: forall a b x y, gle r x a -> gle r b y -> sub (interval_cc r a b) (interval_cc r x y). move=> a b x y xa lby t /Zo_P [tsr [lat tb]]. apply /Zo_P;split => //; split; order_tac. have Hb: forall a b x y, gle r x a -> gle r b y -> sub (interval_cc r a b) (substrate (induced_order r (interval_cc r x y))). by move=> a b x y xa yb; rewrite iorder_sr //; [ apply: Ha | apply: Zo_S]. red; rewrite /scattered_rel; split; last first. move=> y; split; last by case;move=> [yy _]; order_tac. move=> ysr; left;set I:= interval_cc r y y. have Iy: (forall t, inc t I -> t = y). move=> t /Zo_P [_ [t1 t2]]; order_tac. have Isr: (sub I (substrate r)) by apply: Zo_S. split; first (by order_tac); apply /Exercise1_21aP => //. move => u uI ; apply /(Exercise1_21dP) => //; first by apply: sub_trans Isr. by left; move=> a b aI bI; rewrite (Iy _ (uI _ aI)) (Iy _ (uI _ bI)). split; first by (move=> x y; rewrite /scattered_rel; case; [right| left]). move=> y x z; case; move=> [xy sxy]. case; move=> [yz syz]. left; split; [order_tac | apply: (Exercise1_21g tor xy yz sxy syz)]. have xsr: inc x (substrate r) by order_tac. have zsr: inc z (substrate r) by order_tac. case: (tor' _ _ xsr zsr) => xz; [left | right]; split => //. have xx: (gle r x x) by order_tac. move: (Hb _ _ _ _ xx yz) => hs; move: (Exercise1_20a hs sxy). rewrite iorder_trans //; by apply: Ha. have zz: (gle r z z) by order_tac. move: (Hb _ _ _ _ zz xy) => hs; move: (Exercise1_20a hs syz). rewrite iorder_trans // ; by apply: Ha. case; move=> [yz syz]; last first. by right; split; [order_tac | apply: (Exercise1_21g tor yz xy syz sxy) ]. have xsr: inc x (substrate r) by order_tac. have zsr: inc z (substrate r) by order_tac. case: (tor' _ _ xsr zsr) => xz; [left | right]; split => //. have zz: (gle r z z) by order_tac. move: (Hb _ _ _ _ xy zz) => hs; move: (Exercise1_20a hs syz). rewrite iorder_trans //; by apply: Ha. have xx: (gle r x x) by order_tac. move: (Hb _ _ _ _ yz xx) => hs; move: (Exercise1_20a hs sxy). rewrite iorder_trans // ; by apply: Ha. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)