law sub_add_comm

lawful-words@0.1.0.0 · proof_u32.bend:550

import Base

550# (x + m) - y = (x - y) + m for y <= x.
551law sub_add_comm:
552  for +x: Nat
553  for +m: Nat
554  for +y: Nat
555  for +h: {Nat.is_le(y, x) == True{} : Bool}
556  {Nat.sub(Nat.add(x, m), y) == Nat.add(Nat.sub(x, y), m) : Nat}