law lt_dbl

lawful-arrays@0.1.0.0 · proof_base.bend:239

import lawful-arrays@0.1.0.0/proof_base.bend as ProofBase
import Base

239law lt_dbl:
240  for +a: Nat
241  for +b: Nat
242  for e: {Nat.is_lt(a, b) == True{} : Bool}
243  {Nat.is_lt(Nat.add(a, a), Nat.add(b, b)) == True{} : Bool}

Uses (8)

Used by (1)