Theorem one_sub_le_one_sub_mul_one_add

Modification history

2024-09-30 02:32
Mathlib/Algebra/Order/Ring/Defs.lean
feat: When `1 + a ≤ (1 - b) * (1 + c)` (#17214) …
Added one_sub_le_one_sub_mul_one_addView on Github →