~/jendhub

law div_le_self

bend-mathlib@0.8.1.0 · nat.bend:1973

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

1973# A quotient never exceeds the dividend: a / b <= a.
1974law div_le_self:
1975  for a: Nat
1976  for b: Nat
1977  le(Nat.div(a, b), a)

Uses (10)

Used by (0)

No other definition uses this definition.