proposition: Lemma sup_total {E} x : has_sup E -> down E x \/ sup E <= x.
proof: Proof. move=> has_supE; rewrite orC. case: (lerP (sup E) x)=> hx /=; [by left|right]. have /sup_adherent/(_ has_supE) : 0 < sup E - x by rewrite subr_gt0. case=> e Ee hlte; apply/downP; exists e => //; move: hlte. by rewrite opprB addrCA subrr addr0 => /ltW. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid