~/jendhub

law sub_le_sub_left

bend-mathlib@0.8.1.0 · nat.bend:2961

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

2961# Subtracting more gives less: n <= m implies k - m <= k - n.
2962law sub_le_sub_left:
2963  for n: Nat
2964  for m: Nat
2965  for h: le(n, m)
2966  for k: Nat
2967  le(Nat.sub(k, m), Nat.sub(k, n))

Uses (6)

Used by (0)

No other definition uses this definition.