~/jendhub

law div_mul_le_self

bend-mathlib@0.8.1.0 · nat.bend:2130

import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base

2130# The quotient times the divisor never exceeds the dividend: (a / b) * b <= a.
2131law div_mul_le_self:
2132  for a: Nat
2133  for b: Nat
2134  le(Nat.mul(Nat.div(a, b), b), a)

Uses (8)

Used by (1)