law sub_sub_eq

lawful-words@0.1.0.0 · proof_bytes.bend:523

import Base

523law sub_sub_eq:
524  for +j: Nat
525  for +r: Nat
526  for +n: Nat
527  for +hr: {Nat.is_le(r, n) == True{} : Bool}
528  {Nat.sub(j, Nat.sub(n, r)) == Nat.sub(Nat.add(j, r), n) : Nat}