law min_r
import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppendimport 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}
import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppendimport 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}