proposition: Lemma dense_rat (R : realType) : dense (@ratr R @` setT).
proof: Proof. move=> A [r Ar]; rewrite openE => /(_ _ Ar)/nbhs_ballP[_/posnumP[e] reA]. have /rat_in_itvoo[q /itvP qre] : r < r + e%:num by rewrite ltrDl. exists (ratr q) => //; split; last by exists q. apply: reA; rewrite /ball /= distrC ltr_distl qre andbT. by rewrite (@le_lt_trans _ _ r)// ?qre// lerBlDl lerDr ltW. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed