law u32_is_le_nat
import bend-kit-lemmas@0.1.1.0/lemmas.bend as Lemmasimport Base
127law u32_is_le_nat:
128 for a: U32
129 for b: U32
130 {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
import bend-kit-lemmas@0.1.1.0/lemmas.bend as Lemmasimport Base
127law u32_is_le_nat:
128 for a: U32
129 for b: U32
130 {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}