proposition: Theorem sup_in_total_order r X x: total_order r -> sub X (substrate r)-> (least_upper_bound r X x <-> (upper_bound r X x /\ (forall y, glt r y x -> exists z, [/\ inc z X, glt r y z & gle r z x]))).
proof: Proof. move=> tor Xs. have or: order r by move: tor=> []. split. move /(lubP or Xs) => [ub lub]; split=>// y yx. have nu: (~ (upper_bound r X y)). by move=> ys; move: (lub _ ys)=> xy; order_tac. have ysr: (inc y (substrate r)) by order_tac. have [z zX yz]: (exists2 z, inc z X & glt r y z). ex_middle bad; case: nu; split => //. move=> u ux; case: (total_order_pr2 tor ysr (Xs _ ux)) =>// aux. case: bad; ex_tac. by exists z; split => //; move: ub=> [_]; apply. move => [pa pb]; apply/(lubP or Xs); split => //. move=> z ubz. have xs:inc x (substrate r) by case: pa. have zs:inc z (substrate r) by case: ubz. case: (total_order_pr2 tor zs xs) =>// /pb [t [tX yt _]]. case: (not_le_gt or ((proj2 ubz) _ tX) yt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)