law lt_dbl
import lawful-arrays@0.1.0.0/proof_base.bend as ProofBaseimport 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}
import lawful-arrays@0.1.0.0/proof_base.bend as ProofBaseimport 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}