Commit 2025-08-11 10:52 c278b5e3

feat: interval in archimedean field contains fraction with large enough denominator (#27424) This is a slight generalization of exists_rat_btwn that can be used, for instance, to prove that there's a dyadic rational between any two elements.