proposition: Lemma transfinite_aux3 r T x g: worder r -> inc x (substrate r) -> transfiniteg_def (induced_order r (segment r x)) T g -> transfiniteg_def (induced_order r (segmentc r x)) T (g +s1 J x (T (restr g (segment r x)))).
proof: Proof. move=> wo xsr tdo. have or:= proj1 wo. have [sug sog Wg] := tdo. have ssr: sub (segment r x) (substrate r) by apply: sub_segment. have sio: substrate (induced_order r (segment r x)) = segment r x by rewrite iorder_sr. rewrite sio in sog Wg. set tsx:= segmentc r x; set h:= (restr g (segment r x)). have stsx: sub tsx (substrate r) by apply: sub_segmentc. have sioc: substrate (induced_order r tsx) = tsx by rewrite iorder_sr. have nxsg: ~ (inc x (domain g)) by rewrite sog; aw; apply: not_in_segment. have sto := (fgraph_setU1 (T h) sug nxsg). have tos:(segment r x) +s1 x = tsx by rewrite /tsx segmentc_pr. have soto: domain (g +s1 J x (T h)) = tsx by rewrite domain_setU1 sog. hnf;rewrite sioc; split => // y ytsx. rewrite (segment_induced_a (segmentc_segment _ or) ytsx). case: (equal_or_not y x) => yx. rewrite /h yx setU1_V_out //; congr T; apply: restr_exten. move => t ts /=; rewrite setU1_V_in //; ue. have ysx: inc y (segment r x) by move: ytsx; rewrite -tos; case/setU1_P. have ydg: inc y (domain g) by ue. rewrite (setU1_V_in _ sug nxsg ydg) (Wg _ ysx); congr T. rewrite (segment_induced_a (segment_segment _ or) ysx). have sg : segmentp r (domain g) by rewrite sog; apply:segment_segment. apply: restr_exten => t /(lt_in_segment2 sg ydg) tdg. by rewrite (setU1_V_in _ sug nxsg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)