law min_add

lawful-bytes@0.1.1.0 · proof_fast_find2.bend:118

import lawful-bytes@0.1.1.0/proof_fast_find2.bend as ProofFastFind2
import Base

118law min_add:
119  for +o: Nat
120  for +a: Nat
121  for +b: Nat
122  {Nat.min(Nat.add(o, a), Nat.add(o, b)) == Nat.add(o, Nat.min(a, b)) : Nat}

Uses (3)

Used by (1)