proposition: Lemma Exercise2_2a r (B:= Zo (\Po (substrate r)) (fun z=> worder (induced_order r z))) (sso := Zo (coarse B)(fun z=> segmentp (induced_order r (Q z)) (P z))): order r -> (order_on sso B /\ inductive sso).
proof: Proof. move=> or. have HaP: forall x y, gle sso x y <-> [/\ inc x B, inc y B & segmentp (induced_order r y) x]. move=> x y; split; first by move => /Zo_P [] /setXp_P []; aw. move => [pa pb pc]; apply /Zo_P;split => //; [ by apply /setXp_P | by aw ]. have Hb: sgraph sso by move=> t => /Zo_P [] /setX_P []. have Hc: forall x y, gle sso x y -> sub x y. move=> x y => /HaP [_ ] /Zo_P [] /setP_P ysr _; case; rewrite iorder_sr //. have Hf: forall x, inc x B -> sub x (substrate r). by move=> x /Zo_P [ ] /setP_P. have Hd: forall x, inc x B -> gle sso x x. move=> x xB; apply /HaP; split => //;split; first by rewrite iorder_sr; fprops. by move=> a b ax /(iorder_gle3); case. have He:substrate sso = B. set_extens t. by case /(substrate_P Hb) => [] [y] /Zo_P [] /setXp_P []. move=> /Hd; rewrite /gle=> Js ; substr_tac. have os: order sso. split => //. move => t; rewrite He; apply: Hd. move => y x z /HaP [xB yB [xs p1]] /HaP [_ zB [ys p2]]. apply /HaP;split => //; move: (Hf _ xB)(Hf _ yB)(Hf _ zB) => xs1 ys1 zs1. move: xs ys; rewrite iorder_sr // => xs ys. split; first by aw ; apply: (@sub_trans y). move=> a b ax p3; move: (iorder_gle1 p3) (iorder_gle3 p3)=> ba [bz az]. apply: (p1 _ _ ax); apply /iorder_gle0P => //; last by apply: xs. by apply: (p2 _ _ (xs _ ax)); aw. by move => // x y r1 r2; apply: extensionality; apply: Hc. split => //. red;rewrite He => X XE toi. have su: (sub (union X) (substrate r)). move=> t /setU_P [y ty yX]; exact: (Hf _ (XE _ yX)). move: (iorder_osr or su) => [o1 sr1]. have woi: worder (induced_order r (union X)). split => //; rewrite sr1. move => x xu [a ax];move: (xu _ ax) => /setU_P [b ab bX]. set (Z := x \cap b). have neZ:(nonempty Z) by exists a; apply: setI2_i. move: (XE _ bX) => /Zo_P [] /setP_P bsr [wo1 ]; rewrite iorder_sr // =>wo2. have p1: (sub Z b) by apply: subsetI2r. move: (wo2 _ p1 neZ) => [y]; aw; rewrite iorder_trans //. have Z1: (sub Z (substrate r)) by apply: (sub_trans p1). have xr: sub x (substrate r) by apply: sub_trans su. rewrite iorder_trans //; move=> []; rewrite iorder_sr//; move=> yZ yp. have yx:= (@setI2_1 x b _ yZ). exists y; red;rewrite iorder_sr //; split => // z zx; aw. move: (xu _ zx) => /setU_P [t zt tX]. move: toi => [toi1]; rewrite iorder_sr //; last by ue. move=> aux; move: (aux _ _ tX bX). case => h1; move:(iorder_gle1 h1) => h2;move: (Hc _ _ h2) => h3. have zZ: inc z Z by apply: setI2_i => //; apply: h3. apply /iorder_gle0P => //. exact:(iorder_gle1 (yp _ zZ) ). have yb: inc y b by apply: p1. have yt: inc y t by apply: h3. move :(XE _ tX) => /Zo_P [xx wor]. have st: sub t (substrate r) by move: xx => /setP_P. move: (worder_total wor) => [_ ]; rewrite iorder_sr // => tor. apply /iorder_gle0P => //. case: (tor _ _ yt zt)=> h4; first exact: (iorder_gle1 h4). move: h2 => /HaP [_ _ [_ se]]. move: (se _ _ yb h4) => zb. have zZ: inc z Z by apply: setI2_i => //; apply: h3. exact: (iorder_gle1(yp _ zZ)). have uXb:inc (union X) B by apply: Zo_i => //; apply /setP_P. exists (union X); split; first by rewrite He. move => y yX; apply /HaP;split;fprops. split; first by rewrite iorder_sr//; apply: setU_s1 => //. move=> u v uy uv; move: (iorder_gle1 uv) => vu. move:(iorder_gle3 uv)=> [vU uU]. move: vU => /setU_P [w uw wX]. move:toi => [_ ]; rewrite iorder_sr //; last by ue. move=> h; move: (h _ _ yX wX). case => h1; move: (iorder_gle1 h1) => aux; move: (Hc _ _ aux); last by apply. move: aux => /HaP [yB wB [s1 s2]] yw. apply: (s2 _ _ uy); apply /iorder_gle0P=> //; apply: yw; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)