law le_sub_add

lawful-words@0.1.0.0 · proof_nat.bend:923

import Base

923# k <= m gives k + (m - k) = m.
924law le_sub_add:
925  for +k: Nat
926  for +m: Nat
927  for h: {Nat.is_le(k, m) == True{} : Bool}
928  {Nat.add(k, Nat.sub(m, k)) == m : Nat}