law le_add_sub

lawful-words@0.1.0.0 · proof_nat.bend:1469

import Base

1469# m <= k + (m - k).
1470law le_add_sub:
1471  for +m: Nat
1472  for +k: Nat
1473  {Nat.is_le(m, Nat.add(k, Nat.sub(m, k))) == True{} : Bool}