proposition: Lemma Exercise1_21g r x y z: total_order r -> gle r x y -> gle r y z-> scattered (induced_order r (interval_cc r x y)) -> scattered (induced_order r (interval_cc r y z)) -> scattered (induced_order r (interval_cc r x z)).
proof: Proof. move=> tor xy yz scxy scyz. move: (tor) => [or tor']. have xz:(gle r x z) by order_tac. have sxz:sub (interval_cc r x z) (substrate r) by apply: Zo_S. have sxy:sub (interval_cc r x y) (substrate r) by apply: Zo_S. have syz:sub (interval_cc r y z) (substrate r) by apply: Zo_S. move: scxy scyz => /(Exercise1_21aP or sxy) scxy /(Exercise1_21aP or syz) scyz. apply /(Exercise1_21aP or sxz) => u uxz. case: (p_or_not_p (without_gaps (induced_order r u))) =>// wg. have us: (sub u (substrate r)) by apply: sub_trans sxz. set (u1 := u \cap (interval_cc r x y)). set (u2 := u \cap (interval_cc r y z)). have su1: sub u1 (interval_cc r x y) by apply: subsetI2r. have su2: sub u2 (interval_cc r y z) by apply: subsetI2r. have up1: forall t, inc t u -> gle r t y -> inc t u1. move=> t tu ty; move: (uxz _ tu) => /Zo_P [t1 [t2 t3]]. apply: setI2_i => //;apply: Zo_i => //. have up2: forall t, inc t u -> gle r y t -> inc t u2. move=> t tu ty; move: (uxz _ tu) => /Zo_P [t1 [t2 t3]]. apply: setI2_i => //;apply: Zo_i => //. apply /(Exercise1_21dP tor us). case: (p_or_not_p (exists x y, glt (induced_order r u) x y)); last first. by move /(Exercise1_21cP tor us); left. move=> [a [b ltab]]; right. move: (iorder_gle4 ltab) (iorder_gle2 ltab) => [au bu] ltab1. exists a, b; split => // t tu. case: (tor' _ _ (us _ au) (us _ tu)) => ta; last by left. case: (tor' _ _ (us _ tu) (us _ bu)) => tb; last by right. have ysr: inc y (substrate r) by order_tac. move: (scxy _ su1) (scyz _ su2) => wg1 wg2. case: (tor' _ _ ysr (us _ tu)) => ty. move: (up2 _ tu ty) (up2 _ bu (order_transitivity or ty tb)) => t2 b2. case: (equal_or_not t b); first by move => ->; right; order_tac; order_tac. move=> bt1; have bt: glt r t b by order_tac. case: wg2; apply: Exercise1_21e => //; exists t, b; split => //. move: (up1 _ tu ty) (up1 _ au (order_transitivity or ta ty )) => t2 b2. case: (equal_or_not a t); first by move => ->; left; order_tac; order_tac. move=> at1; have at2: glt r a t by order_tac. by case: wg1; apply: Exercise1_21e => //; exists a, t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)