law min_nlt

lawful-words@0.1.0.0 · proof_u32.bend:903

import lawful-words@0.1.0.0/proof_u32.bend as ProofU32
import Base

903law min_nlt:
904  for +x: Nat
905  for +y: Nat
906  for +h: {Nat.is_lt(x, y) == False{} : Bool}
907  {Nat.min(x, y) == y : Nat}

Uses (7)

Used by (1)