law sub_le
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
724# Truncated subtraction never increases: n - m <= n.
725law sub_le:
726 for n: Nat
727 for m: Nat
728 le(Nat.sub(n, m), n)
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
724# Truncated subtraction never increases: n - m <= n.
725law sub_le:
726 for n: Nat
727 for m: Nat
728 le(Nat.sub(n, m), n)