Commit 2024-02-22 09:41 d67f7a69

feat: Add mul_inv and inv_mul versions of div_le_one_of_le (#10597) These are exactly div_le_one_of_le with a / b replaced by a * b⁻¹ and b⁻¹ * a. They come up frequently because some tactics produce inverses as normal forms over division. The iff versions with 0 < b already exist as mul_inv_le_one_iff and inv_mul_le_one_iff; the point of these is to have a weaker nonnegativity assumption on b.