proposition: Lemma Exercise1_21q r: total_order r -> let r' := quotient_order r (scattered_equiv r) in small_set (substrate r') \/ without_gaps r'.
proof: Proof. move=> tor r'. move: (Exercise1_21m tor)(Exercise1_21o tor) => Ha Hb. move: (Exercise1_2g Ha Hb tor) (Exercise1_2h Ha Hb tor)=> qo [oq toq]. simpl in qo; rewrite -/r' in qo oq toq. move: (tor) => [or tor']. set (s:= scattered_equiv r) in *. have Hc:forall a b, gle r a b -> gle r' (class s a) (class s b). move=> a b ab. move: (arg1_sr ab) (arg2_sr ab) => asr bsr. by move: (Exercise1_2j Ha Hb tor asr bsr) => [ok _]; apply: ok. case: (p_or_not_p (small_set (substrate r'))); first by left. move=> nss; right; split => //. ex_middle ne; case: nss => a b asr' bsr'. ex_middle ab; case: (toq _ _ asr' bsr') => cab. by case: ne; exists a, b. by case: ne; exists b, a; split; fprops. move: Ha => [[pr es ss] woc]. have sr': (substrate r' = quotient s) by rewrite /r' substrate_quotient_order. move=> x y xy; move: (xy) => [lexy nxy]. have nsxy: (~ (related s (rep x) (rep y))). apply /related_rr_P =>//;rewrite - sr'; order_tac. ex_middle nez; case: nsxy. move: lexy; rewrite qo; move=> [xq yq lerxy]. apply /graph_on_P1; split => //; try order_tac. left;split => //. have si: (sub (interval_cc r (rep x) (rep y)) (substrate r)) by apply: Zo_S. apply /(Exercise1_21aP or si). have Hx:class s (rep x) = x by apply: class_rep. have Hy:class s (rep y) = y by apply: class_rep. move=> u ui [oi woi1 woi2]. have uxu: (forall a, inc a u -> inc a x \/ inc a y). move=> a au; move: (ui _ au) => /Zo_P [asr [rxa ary]]. move: (Hc _ _ rxa); rewrite Hx => xca. move: (Hc _ _ ary); rewrite Hy => yca. case: (equal_or_not x (class s a)) => xca1. left; rewrite xca1; apply: inc_itself_class => //; ue. have p1: (glt r' x (class s a)) by split. case: (equal_or_not (class s a) y) => yca1. right; rewrite -yca1; apply: inc_itself_class => //; ue. have p2: (glt r' (class s a) y) by split. case: nez; exists (class s a); split => //. move: (class_rep es xq) (class_rep es yq) => c1 c2. have rxsr: (inc (rep x) (substrate r)) by order_tac. have rysr: (inc (rep y) (substrate r)) by order_tac. have Hu:forall a, inc a x -> x = class s a by move=> b bx;apply: is_class_pr. have Hv:forall a, inc a y -> y = class s a by move=> b bx;apply: is_class_pr. have xsr: sub x (substrate r) by rewrite - ss - c1; apply: sub_class_substrate. have ysr: sub y (substrate r) by rewrite - ss - c2; apply: sub_class_substrate. move: (Exercise1_21n tor rxsr); rewrite -/s c1. move: (Exercise1_21n tor rysr); rewrite -/s c2. move /(Exercise1_21aP or ysr) => c3 /(Exercise1_21aP or xsr) c4. set (u1:= u \cap x). have u1x: (sub u1 x) by apply: subsetI2r. have u1sr: (sub u1 (substrate r)) by apply: (sub_trans u1x). move: (c4 _ u1x) => /(Exercise1_21dP tor u1sr) c5. set (u2:= u \cap y). have u2y: (sub u2 y) by apply: subsetI2r. have u2sr: (sub u2 (substrate r)) by apply: (sub_trans u2y). move: (c3 _ u2y) => /(Exercise1_21dP tor u2sr) c6. have p1u: (~(exists a b, [/\ inc a u1, inc b u1 & glt r a b])). move=> [a [b [au1 bu1 ab]]]. case: c5 => c5'; first by move:ab=> [_ ab]; case:ab; exact: (c5' _ _ au1 bu1). move: c5' => [a' [b' [a'u1 b'u1 ab' ie]]]. move: (@subsetI2l u x) => u1x'. have ab'': glt (induced_order r u) a' b' by apply/iorder_gltP; split;fprops. move: (woi2 _ _ ab'') => [c ca cb]. move:(iorder_gle4 ca)(iorder_gle2 ca)(iorder_gle2 cb) => [_ cu] ca' cb'. suff uc1: (inc c u1) by case: (ie _ uc1)=> h; order_tac. apply: setI2_i => //; case: (uxu _ cu) => //cy. move: cb' => [cb'' _]; move: (Hc _ _ cb''). rewrite -(Hv _ cy) - (Hu _ (setI2_2 b'u1)) => bad; order_tac. have p2u: (~(exists a b, [/\ inc a u2, inc b u2 & glt r a b])). move=> [a [b [au1 bu1 ab]]]. case: c6 => c6'; first by move:ab=> [_ ab]; case:ab; exact: (c6' _ _ au1 bu1). move: c6' => [a' [b' [a'u1 b'u1 ab' ie]]]. move: (@subsetI2l u y) => u2y'. have ab'': glt (induced_order r u) a' b' by apply/iorder_gltP; split;fprops. move: (woi2 _ _ ab'') => [c ca cb]. move:(iorder_gle4 ca)(iorder_gle2 ca)(iorder_gle2 cb) => [_ cu] ca' cb'. suff uc2: (inc c u2) by case: (ie _ uc2)=> h; order_tac. apply: setI2_i => //; case: (uxu _ cu) => //cx. move: ca' => [ca'' _]; move: (Hc _ _ ca''). rewrite -(Hu _ cx) - (Hv _ (setI2_2 a'u1)) => bad; order_tac. move: woi1 => [a [b lab]]; move: (woi2 _ _ lab) => [c lac lcb]. move: (iorder_gle4 lac)(iorder_gle4 lcb) => [au cu][_ bu]. move: (iorder_gle2 lac)(iorder_gle2 lcb) => ltac ltcb. have ltab: glt r a b by order_tac. case: (uxu _ au) => axy. have au1: inc a u1 by apply: setI2_i. case: (uxu _ cu) => cxy. case: p1u; exists a, c;split => //; by apply: setI2_i. case: (uxu _ bu) => bxy. case: p1u; exists a, b;split => //; by apply: setI2_i. case: p2u; exists c, b;split => //; by apply: setI2_i. have au2: inc a u2 by apply: setI2_i. case: (uxu _ cu) => cxy. case: (uxu _ bu) => bxy. case: p1u; exists c, b;split => //; by apply: setI2_i. case: p2u; exists a, b;split => //; by apply: setI2_i. case: p2u; exists a, c;split => //; by apply: setI2_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)