sqrt): `sqrt x < y ↔ x < y^2` (#13546)

Commit

3 years ago

feat(data/real/sqrt): `sqrt x < y ↔ x < y^2` (#13546) Prove `real.sqrt_lt_iff` and generalize `real.lt_sqrt`.

Author

YaelDillies

Parents