law sub_eq_zero_of_le

bend-mathlib@0.8.1.0 · nat.bend:1742

import Base

1742# Subtracting a larger number gives zero: a <= b implies a - b = 0.
1743law sub_eq_zero_of_le:
1744  for a: Nat
1745  for b: Nat
1746  for h: le(a, b)
1747  {Nat.sub(a, b) == 0n : Nat}