law min_r

lawful-bytes@0.1.1.0 · proof_fast_append.bend:285

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

285law min_r:
286  for +a: Nat
287  for +b: Nat
288  for +h: {Nat.is_lt(a, b) == False{} : Bool}
289  {Nat.min(a, b) == b : Nat}

Uses (6)

Used by (1)