proposition: Lemma ordinalr_segment (r:relation) a x (b:=ordinalr r x): worder_rc r -> r x x -> a <=o b -> (exists2 y, r y y & a = ordinalr r y).
proof: Proof. move => woc rxx ab. case:(ole_eqVlt ab); [by move ->; exists x | move => /(oltP (proj32 ab)) iab]. have [pa pb] := (worder_rc_seg woc rxx). move: (the_ordinal_iso1 pa) => []. rewrite -/(ordinalr _ _) pb ordinal_o_sr. set gr := (graph_on r (segmentr r x)); set f := (the_ordinal_iso gr). set oor := (ordinal_o (ordinalr r x)). move => sa sb [[[ff injf] [_ sjf]] sf tf] sd. have asf: inc a (source f) by ue. move: (Vf_target ff asf); rewrite tf. set y := Vf f a; set rs:= (graph_on r (segmentr r y)). move /(segmentrP (proj2 woc) rxx) => [ryx xny]. have or:= (proj1 (proj1 woc)). move: (proj33 or _ _ ryx) => [ryy _]. have sP:=(segmentrP (proj2 woc) ryy). set g:= Lf (Vf f) a (segmentr r y). have [oa ob sab] := ab. suff oih:order_isomorphism g (ordinal_o a) rs. have h : ordinal_o a \Is rs by exists g. have tt:= (worder_invariance h (ordinal_o_wor oa)). by exists y => //; rewrite - (ordinal_o_isu2 tt oa (orderIS h)). have srr: substrate rs = (segmentr r y). by apply:graph_on_sr => u /sP [/(proj33 or) []]. have saf: sub a (source f) by ue. have la: lf_axiom (Vf f) a (segmentr r y). move => s ssa; have isf :=(saf _ ssa). move/(oltP oa): ssa => [la na]. apply /sP; split; last by move/(injf _ _ isf asf). have:gle oor s a. by apply /graph_on_P1;rewrite - sf; split => //; case:la. by move /(sd s a isf asf) => /graph_on_P1 []. hnf; rewrite (ordinal_o_sr) srr. split => //; [ fprops | apply: (order_from_rel _ or) | |]. hnf; rewrite /g; saw; apply: lf_bijective => //. by move => u v ua va; apply injf; apply: saf. move => c /sP [c1 c2]. have: inc c (target f). rewrite tf; apply /(segmentrP (proj2 woc) rxx). move: (proj31 or _ _ _ c1 ryx)=> cx; split => //. by move => ecx; rewrite -ecx in ryx;move: (proj32 or _ _ c1 ryx). move /sjf => [d dsf dv]; exists d; last by rewrite dv. have od: ordinalp d by rewrite sf in dsf; exact: (Os_ordinal ob dsf). case:(oleT_si oa od) => // sad. have: gle oor a d by apply /sub_gleP; split => //; ue. move /(sd _ _ asf dsf) => /graph_on_P1 [_ _];rewrite -dv -/y => yc. case: c2; exact (proj32 or _ _ c1 yc). hnf; rewrite /g;aw => u v ua va; rewrite !LfV//. move: (saf _ ua) (saf _ va) =>ub vb. have h:= (sd u v ub vb). split. move/sub_gleP=> [_ _ h1]; apply/graph_on_P1; split; try apply: la => //. suff:gle gr (Vf f u) (Vf f v) by move/graph_on_P1 =>[]. by apply /h; apply/sub_gleP; rewrite - sf. move/graph_on_P1 => [_ _ h1]; apply/sub_gleP; split => //. suff:gle gr (Vf f u) (Vf f v) by move/h /sub_gleP=> []. apply/graph_on_P1; split => //; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)