law le_div_iff_mul_le_sym

bend-mathlib@0.8.1.0 · nat.bend:4083

import Base

4083# A quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a, reversed to rewrite toward the simple side.
4084law le_div_iff_mul_le_sym:
4085  for n: Nat
4086  for +a: Nat
4087  for +b: Nat
4088  {Nat.is_le(Nat.mul(n, 1n+b), a) == Nat.is_le(n, Nat.div(a, 1n+b)) : Bool}