law u32_is_le_nat

bend-kit-lemmas@0.1.1.0 · lemmas.bend:127

import bend-kit-lemmas@0.1.1.0/lemmas.bend as Lemmas
import 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}

Uses (11)

Used by (1)