proposition: Lemma isomorphic_subset_segment r X: worder r -> sub X (substrate r) -> exists2 w, segmentp r w & (induced_order r X) \Is (induced_order r w).
proof: Proof. move => wor asr. move: (proj1 wor) => or. have woi :=(induced_wor wor asr). case: (isomorphism_worder2 woi wor). - move => [f isf]; exists (substrate r). apply: substrate_segment. by exists f; rewrite (iorder_substrate or). - rewrite (iorder_sr or asr). move => [x xa]. have ha:sub (segment (induced_order r X) x) X by apply: sub_segment2. rewrite /seg_order(iorder_trans _ ha); move =>[f fiso]. move:(order_isomorphism_siso fiso) => fsi. move: fiso => [hb _ hc hd]. move:hc; rewrite (iorder_sr or (sub_trans ha asr)); move =>[bf sf tf]. pose E := Zo (substrate r) (fun z => glt r (Vf (inverse_fun f) z) z). have xsr := asr _ xa. have Esr: sub E (substrate r) by apply: Zo_S. have neE: nonempty E. exists x; apply: (Zo_i xsr). rewrite -tf in xsr;move: (inverse_Vis bf xsr); rewrite sf =>/segmentP. by move/iorder_gle2. move: (worder_prop wor Esr neE) =>[y /Zo_P[ysr lt1] yl]. set z := (Vf (inverse_fun f) y). move:(arg1_sr (proj1 lt1)) => zsr. suff /yl eZ: inc z E by move: (not_le_gt or eZ lt1). have ytf: inc y (target f) by ue. apply: (Zo_i zsr). rewrite -/z. set t := (Vf (inverse_fun f) z). move: (inverse_V bf ytf); rewrite -/z => yv. rewrite -tf in zsr;move: (inverse_Vis bf zsr); rewrite -/z -/t => tsf. move: (inverse_V bf zsr); rewrite -/z -/t => zv. move: lt1; rewrite -/z - yv -{1} zv => lt2. by move/ (fsi t z tsf (inverse_Vis bf ytf)): lt2 => /iorder_gltP [_ _ ]. - move => [x xE /orderIS ww]. by exists (segment r x) => //; apply: (segment_segment _ or). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)