mathlib3

464e1ddc - feat(data/real/ereal): positive covariance typeclasses (#18157)

feat(data/real/ereal): positive covariance typeclasses (#18157) There is no semiring structure on `ereal`, but we can prove results about monotonicity of multiplication by positive elements. This PR adds some lemmas and typeclass `pos_mul_mono` `mul_pos_mono` `pos_mul_reflect_lt` `mul_pos_reflect_lt` for `ereal`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>