proposition: Theorem compare_inf_sup2 r A: order r -> sub A (substrate r) -> has_supremum r A -> has_infimum r A -> nonempty A -> gle r (infimum r A) (supremum r A).
proof: Proof. move=> or As hs hi [x xA]. move /(lubP or As): (supremum_pr1 or hs) => [[uE p1] _ ]. move /(glbP or As): (infimum_pr1 or hi) => [[vE p2] _]. move: (p1 _ xA)(p2 _ xA)=> q1 q2; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)