proposition: Lemma transfinite_exists1 r T: worder r -> exists f, (transfiniteg_def r T f).
proof: Proof. move => wo. set (s:=Zo (segments r) (fun z => exists f, transfiniteg_def (induced_order r z) T f)). have or:= proj1 wo. have als: (alls s (segmentp r)) by move=> x /Zo_S /(inc_segmentsP wo). have ssu: forall s', sub s' s -> inc (union s') s. move=> s' s's. have als':(alls s' (segmentp r)) by move=> x xs'; apply: (als _ (s's _ xs')). apply: Zo_i; first by apply /(inc_segmentsP wo); apply: setU_segment. pose tdf z:= transfiniteg_defined (induced_order r z) T. exists (unionf s' tdf); apply: (transfinite_aux2 wo als'). by move=> z zs'; move: (s's _ zs') => /Zo_P [p1 /choose_pr]. have sss x:inc x (substrate r) -> inc (segment r x) s -> inc (segmentc r x) s. move=> xst /Zo_hi [f tdf]; apply: Zo_i. by apply: segmentc_insetof. exists (f +s1 J x (T (restr f (segment r x)))). apply: (transfinite_aux3 wo xst tdf). by move /Zo_hi: (transfinite_principle2 wo ssu sss);rewrite iorder_substrate. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)