proposition: Theorem compare_inf_sup1 r A: order r -> sub A (substrate r) -> has_supremum r A -> has_infimum r A -> A = emptyset -> (greatest r (infimum r A) /\ least r (supremum r A)).
proof: Proof. move=> or As /(supremum_pr1 or) hs /(infimum_pr1 or) hi Ae. move: hs hi; rewrite Ae glb_set0 // lub_set0 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)