~/jendhub

law sub_le_sub_right

bend-mathlib@0.8.1.0 · nat.bend:2977

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

2977# Subtraction on the right preserves the order: n <= m implies n - k <= m - k.
2978law sub_le_sub_right:
2979  for n: Nat
2980  for m: Nat
2981  for h: le(n, m)
2982  for k: Nat
2983  le(Nat.sub(n, k), Nat.sub(m, k))

Uses (8)

Used by (0)

No other definition uses this definition.