proposition: Lemma segment_r_succ_or_limit r x: worder r -> inc x (substrate r) -> [\/ (segment_r r x = substrate r), (exists2 z, inc z (segment r x) & segment_r r x = segment_r r z -s1 z) | (segment_r r x) = intersection (fun_image (segment r x) (segment_r r)) ].
proof: Proof. move => wor xsr. have tor:= (worder_total wor). have or := proj1 wor. set T := segment r x. case: (emptyset_dichot T) => te. by move: (segment_rC tor xsr); rewrite -/T te setC_0 => h; constructor 1. have TE: sub T (substrate r) by apply: sub_segment. have Tb: bounded_above r T by exists x; split => // y /segmentP []. move: (worder_hassup wor TE Tb) => [z /(lubP or TE) [[za zb] zc]]. case: (inc_or_not z T) => zT. constructor 2; ex_tac. have ltx: glt r z x by apply /segmentP. set_extens u. move /segment_rP => l1. have [l2 /nesym n2]: glt r z u by order_tac. by apply/setC1_P; split => //;apply /segment_rP. move => /setC1_P [/segment_rP qa qb]; apply /segment_rP. have uE: inc u (substrate r) by order_tac. case: (equal_or_not u x) => eq; first by rewrite eq; order_tac. case: (proj2 tor _ _ xsr uE) => // le1. move /segmentP: (conj le1 eq) => /zb le2; case: qb; order_tac. constructor 3. have nf: nonempty (fun_image T (segment_r r)) by apply:funI_setne. set_extens t. move /segment_rP => h; apply /(setI_P nf) => i /funI_P [u /segmentP zu ->]. move: zu => [zu _];apply /segment_rP; order_tac. move => /(setI_P nf) h; apply /segment_rP. have hh: forall q, inc q T -> gle r q t. move => q qt;apply /segment_rP; apply: h; apply/funI_P; ex_tac. have tE: inc t (substrate r) by move: te => [u /hh ut]; order_tac. have zt : gle r z t by apply:zc; split => //; apply: hh. case: (equal_or_not z x) => eq; first by rewrite - eq. have zE: inc z (substrate r) by order_tac. case: (proj2 tor _ _ xsr zE) => // le1;first order_tac. by case: zT; apply /segmentP. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)