law dbl_le

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

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

52law dbl_le:
53  for +n: Nat
54  for +x: Nat
55  for +y: Nat
56  {Nat.is_le(U.U32Nat.dbl(n, x), U.U32Nat.dbl(n, y)) == Nat.is_le(x, y) : Bool}