proposition: Lemma le_inf A B : -%R @` B `<=` down (-%R @` A) -> nonempty B -> has_inf A -> inf A <= inf B.
proof: Proof. move=> SBA AB Ai; rewrite lerNl opprK le_sup// ?has_inf_supN//. exact/nonemptyN. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid