proposition: Lemma has_inf_supN E : has_sup (-%R @` E) <-> has_inf E.
proof: Proof. split=> [ [NEn0 [x /ub_lbN xubE]] | [En0 [x /lb_ubN xlbe]] ]. by split; [apply/nonemptyN|rewrite -[E]setNK; exists (- x)]. by split; [apply/nonemptyN|exists (- x)]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid