proposition: Lemma lt_inf_imfset {T : Type} (F : T -> R) l : has_inf [set y | exists x, y = F x] -> inf [set y | exists x, y = F x] < l -> exists2 x, F x < l & inf [set y | exists x, y = F x] <= F x.
proof: Proof. set P := [set y | _]; move=> hs; rewrite -subr_gt0. move=> /inf_adherent/(_ hs)[_ [x ->]]; rewrite addrCA subrr addr0 => ltFxl. by exists x=> //; move/lbP : (inf_lower_bound hs) => -> //; exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid