law dbl_lt

bend-osdev-u32@0.1.0.0 · LAWS.bend:46

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

46law dbl_lt:
47  for +n: Nat
48  for +x: Nat
49  for +y: Nat
50  {Nat.is_lt(U.U32Nat.dbl(n, x), U.U32Nat.dbl(n, y)) == Nat.is_lt(x, y) : Bool}