proposition: Theorem inf_in_total_order r X x: total_order r -> sub X (substrate r)-> (greatest_lower_bound r X x <-> (lower_bound r X x /\ (forall y, glt r x y -> exists z, [/\ inc z X, glt r z y & gle r x z]))).
proof: Proof. move=> tor Xs. have or: order r by move: tor=> []. split. move /(glbP or Xs) => [ub lub]; split=>// y yx. have nu: (~ (lower_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 z y). ex_middle bad;case: nu; split =>// u ux. case: (total_order_pr2 tor (Xs _ ux) ysr) =>// aux. case: bad; ex_tac. by exists z; split => //; move: ub=> [_]; apply. move => [ub lub]; apply/(glbP or Xs); split => // z ubz. have xs:inc x (substrate r) by case: ub. have zs:inc z (substrate r) by case: ubz. case: (total_order_pr2 tor xs zs) =>// /lub [t [tX yt tx]]. case: (not_le_gt or ((proj2 ubz) _ tX) yt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)