law add_complement

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/map_difference_order.bend:52

import Base

52law add_complement:
53  for n: Nat
54  for m: Nat
55  for bound: {Nat.is_le(m, n) == True{} : Bool}
56  {Nat.add(m, Nat.sub(n, m)) == n : Nat}