law min_l

lawful-bytes@0.1.1.0 · proof_fast_append.bend:269

import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppend
import Base

269law min_l:
270  for +a: Nat
271  for +b: Nat
272  for +h: {Nat.is_lt(a, b) == True{} : Bool}
273  {Nat.min(a, b) == a : Nat}

Uses (6)

Used by (1)