~/jendhub

law mod_le

bend-mathlib@0.8.1.0 · nat.bend:1953

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

1953# A remainder never exceeds the dividend: a % b <= a.
1954law mod_le:
1955  for a: Nat
1956  for b: Nat
1957  le(Nat.mod(a, b), a)

Uses (11)

Used by (0)

No other definition uses this definition.