proposition: Lemma union_segments r (E := substrate r)(A := union (segmentss r)): total_order r -> ( (forall x, ~ (greatest r x)) -> A = E) /\ (forall x, greatest r x -> A = E -s1 x).
proof: Proof. move=> tor. have Ap: forall x, inc x A <-> exists y, glt r x y. move=> x;split. move/setU_P => [y xy /funI_P [z zE sy]]. exists z; apply: inc_segment;ue. move=> [y xy]; apply/setU_P;exists (segment r y). by apply: segment_inc=>//; order_tac. apply/funI_P; exists y => //; rewrite /E; order_tac. have AE: sub A E by move=> t /Ap [y xy]; rewrite /E;order_tac. split. move=> p; apply: extensionality=>// t tE. apply /Ap; ex_middle bad; case: (p t); split =>//. move=> y ysr; case: (total_order_pr2 tor tE ysr)=>//. by move=> ty; case: bad; exists y. move=> x [xs gr]; set_extens y => ys. apply/setC_P;split; first by apply: AE. move=> /set1_P xy; move: ys => /Ap [z yz]. have zc: inc z (substrate r) by order_tac. move: (gr _ zc) => aux. rewrite xy in yz; move:tor=> [or _];order_tac. move /setC_P: ys => [yE] /set1_P yx. by apply/Ap; exists x; split=>//; apply: gr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)