law le_of_add_eq

bend-mathlib@0.8.1.0 · nat.bend:1822

import Base

1822# A witnessed difference gives the order: a + k = b implies a <= b.
1823law le_of_add_eq:
1824  for a: Nat
1825  for k: Nat
1826  for -b: Nat
1827  for e: {Nat.add(a, k) == b : Nat}
1828  le(a, b)