~/jendhub

law sub_pos_of_lt

bend-mathlib@0.8.1.0 · nat.bend:3013

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

3013# A difference is positive below the minuend: m < n implies 0 < n - m.
3014law sub_pos_of_lt:
3015  for m: Nat
3016  for n: Nat
3017  for h: lt(m, n)
3018  lt(0n, Nat.sub(n, m))

Uses (4)

Used by (0)

No other definition uses this definition.