proposition: Lemma inf_lt (S : set R) (x : R) : S !=set0 -> (inf S < x -> exists2 y, S y & y < x)%R.
proof: Proof. move=> /nonemptyN S0; rewrite /inf ltrNl => /sup_gt => /(_ S0)[r [r' Sr']]. by move=> <-; rewrite ltrNr opprK => r'x; exists r'. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid