proposition: Lemma lt_sup_imfset {T : Type} (F : T -> R) l : has_sup [set y | exists x, y = F x] -> l < sup [set y | exists x, y = F x] -> exists2 x, l < F x & F x <= sup [set y | exists x, y = F x].
proof: Proof. set P := [set y | _] => hs; rewrite -subr_gt0. move=> /sup_adherent/(_ hs)[_ [x ->]]; rewrite subKr=> lt_lFx. by exists x => //; move/ubP : (sup_upper_bound hs) => -> //; exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid