proposition: Lemma isomorphism_worder_sub r E (r' := induced_order r E): worder r -> sub E (substrate r) -> iso_seg_iso r' r (iso_seg_fun r' r).
proof: Proof. move => wor sr; move: (proj1 wor) => or. move: (induced_wor wor sr) => wor'. move: (iorder_sr (proj1 wor) sr) => sr'. move: (iso_graph_prop wor' wor). set f := iso_seg_fun _ _;move => [[sa sb] st di]. rewrite sr' in sa. rewrite (iorder_trans _ sa) => is1; split => //. case: di => qa; first by move: is1; rewrite qa sr'. move: is1; rewrite qa (iorder_substrate or). move => ts1; move:(ts1) =>[or1 _ [[injf [ff srjf]] sf tf] fi]. set X := Zo (source f) (fun x => glt r x (Vf f x)). case: (emptyset_dichot X) => xe; last first. have Xsr: sub X (substrate r) by move => t /Zo_S/sa/sr. move: (worder_prop wor Xsr xe) => [a /Zo_P[asr [le1 ne1]] ap]. move :(arg1_sr le1) => gasr. have atf: inc a (target f) by ue. move: (srjf a atf) => [b bsf bv]. move: le1; rewrite {1} bv. move/(fi b a bsf asr) => /iorder_gleP [ra rb rc]. have aux: a <> b by move => bb; case: ne1; rewrite {2} bb. have /ap le2: inc b X. apply: (Zo_i bsf); split => //; try ue. by move: (not_le_gt or rc (conj le2 aux)). have eq2: (source f) = E. apply: extensionality => // a tE; ex_middle bad. move: (sr _ tE) => asr. have tsg: inc a (target f) by ue. move: (srjf _ tsg) => [b bsf bv]. have bE: inc b E by apply: sa. move:(sr _ bE) => bsr. case: (total_order_pr2 (worder_total wor) bsr asr) => h. by empty_tac1 b; apply:(Zo_i bsf); rewrite - bv. have aux: gle (induced_order r E) a b. by apply/iorder_gleP. exact:(sb b a bsf aux). by move: ts1; rewrite /r' eq2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)