proposition: Lemma olex_G_cc (m:= cst_graph (substrate r') olexp_lE) (comp:= ocomparable olexp') (G := (connected_comp comp (substrate olexp') m)) : nonempty (substrate r) -> olexp_G = G.
proof: Proof. move=> nsr. move: (olexp_G_least nsr) => []; rewrite -/m (proj2 olexp_osr) => qa qb. set_extens t. move=> tG; move: (olexp_Gs tG) => ts. move: (qb _ tG) => le1; move: (iorder_gle1 le1) => le2. have cmt: comp m t by left. move: tG => /Zo_P [pa pb]. rewrite /G; apply setI_i. exists (substrate olexp'); apply: Zo_i. apply: Zo_i; [ aw;fprops |by move=> a b _ /setC_P []]. apply :setP_Ti. by apply: olexp_Gs. move=> y => /Zo_P [] /Zo_P [pc pd] pe. case: (inc_or_not t y) => nty //. have pf: inc t ((substrate olexp') -s y) by apply /setC_P. move: (pd _ _ pe pf) => bad; contradiction. have or': order olexp' by apply: (proj1 olexp'_osr). set E :=(substrate olexp'). have pb: symmetric_r comp by move => a b /=; case;[right | left]. have pc: (forall x y : Set, comp x y -> inc x E). rewrite /comp /E; move => x y; case=> auxl; order_tac. have pa: reflexive_re comp E. move => y; split; last by apply: pc. by move => yE; left; order_tac. have mE: inc m E by apply: (olexp_Gs qa). rewrite /G - (connected_comp_class pa pb pc mE). case: (chain_equivalence_eq pa pb pc). set Sg := chain_equivalence comp E; move => es ss. move /(class_P es) => /graph_on_P1 [_ _ [c [cc]]]. suff haux: forall a b, comp a b -> inc a olexp_G -> inc b olexp_G. move=> h; move <-; move: qa; rewrite -h; clear h. move: cc;elim: c => // b c /=. move => hrec [pd pe] bG; move: (haux _ _ pd bG); apply: (hrec pe). move => a b cab. case: (equal_or_not a b) => ab; first by rewrite ab. set T := olex_nsv r' a b. set S:= (gfunctions (substrate r') (substrate r)). set r'' := induced_order (opp_order r') T. have [ais [bis wor'']]: inc a S /\ inc b S /\ worder r''. move: cab;case; move /olexp'_gleP; move=> [ra rb rc]; split => //. by case: rc => //=; case. case: rc; first by move=> ba; case: ab. by simpl;rewrite olex_nsvS -/r''; case. move /Zo_P => [pe pf]; apply: Zo_i => //. have pg: sub (olexp_I b) ((olexp_I a) \cup T). move => z /Zo_P [ph h]; apply /setU2_P. case: (equal_or_not (Vg a z) olexp_lE) => eq1; last by left; apply /Zo_P. by right; apply: Zo_i => //; rewrite eq1; apply:nesym. apply: (sub_finite_set pg); apply: finite_union2 => //. move: (wor') => [or1 _]. have Ts: sub T (substrate r') by apply: Zo_S. move: (wor'') => [sa _]; move: (opp_osr sa) => [xa xb]. move: (opp_osr or1) => [ya yb]. have o2: opp_order r'' = induced_order r' T. move: (iorder_osr or1 Ts) => [ob sob]. apply (order_exten xa ob) => x y; split. move /opp_gleP /iorder_gleP => [ta tb] /opp_gleP tc. by apply /iorder_gleP. move /iorder_gleP =>[ta tb tc]; apply /opp_gleP /iorder_gleP. by split => //; apply /opp_gleP. have wo2: worder (opp_order r''). by rewrite o2; apply: induced_wor => //; apply: Zo_S. move: (well_ordered_opposite wor'' wo2). rewrite /r'' iorder_sr//; fprops; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)