law le_div_iff_mul_le

bend-mathlib@0.8.1.0 · nat.bend:941

import Base

941# A quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a.
942law le_div_iff_mul_le:
943  for n: Nat
944  for +a: Nat
945  for +b: Nat
946  {Nat.is_le(n, Nat.div(a, 1n+b)) == Nat.is_le(Nat.mul(n, 1n+b), a) : Bool}