proposition: Lemma olex_cc_tor (r':= olex r g): (allf g total_order) -> forall x, inc x (substrate r') -> total_order (induced_order r' (connected_comp (ocomparable r') (substrate r') x)).
proof: Proof. move: olex_osr => [or' sr] h. set E :=(substrate r'); set c := ocomparable r'. have pa: reflexive_re c E. rewrite /E /r' sr. move => y;split. by move => yE; left; apply /olex_gleP; apply: olex_R. by case; move /olex_gleP => [ok _]. have pb: symmetric_r c by move => a b /=; case; [right | left]. have pc: (forall x y, c x y -> inc x E). rewrite /c /ocomparable /E; move => x y; case=> auxl; order_tac. move => x xE; rewrite - (connected_comp_class pa pb pc xE). case: (chain_equivalence_eq pa pb pc). set Sg := chain_equivalence c E; move => es ss. move:(sub_class_substrate es (x:=x)); rewrite ss => pd. move: (iorder_osr or' pd) => [pa1 pb1]. split => //;rewrite pb1 => a b ac bc. suff: c a b by case => h1; [ left | right]; apply /iorder_gleP. have: related Sg a b. move: ac bc => /(class_P es) s1 /(class_P es) s2. have s3: related Sg a x by equiv_tac. equiv_tac. move/graph_on_P1 => [_ _ [xc [cc <- <-] ]] {a b ac bc}. elim: xc cc; first by move=> a b //. move=> u xc Hrec; simpl; move => [cuh cc]; move: (Hrec cc) => c1. apply: ((olex_cc_comparable2 h) _ _ _ cuh c1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)