proposition: Lemma transfinite_principle1 x: segmentp r x -> inc x s.
proof: Proof. move=> sx. have or: order r by case: wor. move: (segments_worder wor) => woi. set (cs:= (segments r) -s s). case: (emptyset_dichot cs) => necs. have nc: (~ inc x cs) by rewrite necs; case; case. move: sx => /(inc_segmentsP wor) sx. apply: (nin_setC sx nc). have scs: sub cs (segments r) by rewrite /cs; apply: sub_setC. move:(proj2 (sub_osr (segments r))) => sr1. move: (scs); rewrite - {1} sr1 => src1. move:(worder_prop woi src1 necs) => [y ycs hyp]. move/setC_P:(ycs) => [yssr nys]. have ysr:(sub y (substrate r)) by apply: sub_segments=>//. have woi': worder (induced_order r y) by apply: induced_wor. case: (p_or_not_p (exists a, greatest_induced r y a)). move=> [a []]; rewrite iorder_sr // => [ay pa]. move: (ysr _ ay)=> asr. have ysc: (y = segmentc r a). set_extens t => ts; first by move: (iorder_gle1 (pa _ ts)) => /segmentcP. move: ts => /segmentcP ta. move: yssr => /(inc_segmentsP wor) [_ aux]; apply: (aux _ _ ay ta). case: (p_or_not_p (inc (segment r a) cs))=> h. move: (hyp _ h) => /sub_gleP [_ _ ysa]. case: (not_in_segment (ysa _ ay)). have p1: (inc (segment r a) (segments r)) by apply: segment_insetof. by case: nys; rewrite ysc; apply: adj_stable =>//; apply: (nin_setC p1 h). move=> nge. have aux: (forall x, ~ greatest_induced r y x). by move=> b ngeb; case: nge; exists b. move: (union_segments (worder_total woi'))=> [unm _]. move: (unm aux); rewrite iorder_sr // => us; clear aux unm. case: nys; rewrite -us; apply: u_stable. move => z /funI_P [u uy zv]. case: (inc_or_not z cs) => zcs. move: (hyp _ zcs) => /sub_gleP [_ _ yz]. move: uy; rewrite iorder_sr // => uy; move: (yz _ uy). by rewrite zv=>/not_in_segment. have siu: (segmentp (induced_order r y) z). rewrite zv; apply: segment_segment; fprops. have zsr: (inc z (segments r)). apply /(inc_segmentsP wor). move: yssr => /(inc_segmentsP wor) yssr. apply: (subsegment_segment or yssr siu). by apply: (nin_setC zsr zcs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)