~/jendhub

law div_le_div_left

bend-mathlib@0.8.1.0 · nat.bend:3447

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

3447# Division is antitone in a positive divisor: 0 < s and s <= t imply a / t <= a / s.
3448law div_le_div_left:
3449  for a: Nat
3450  for s: Nat
3451  for t: Nat
3452  for hs: lt(0n, s)
3453  for h: le(s, t)
3454  le(Nat.div(a, t), Nat.div(a, s))

Uses (14)

Used by (1)