def ucmp_nat

bend-kit-collections@0.1.4.1 · PROOF.bend:3990

import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF

import Base
import bend-kit-lemmas@0.1.1.0/lemmas.bend as Lemmas

3990def ucmp_nat(+a: U32, +b: U32) -> {Nat.cmp(U32.to_nat(a), U32.to_nat(b)) == U32.cmp(a, b) : Cmp}:
3991  Equal.sym(Cmp, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), Lemmas.u32_cmp_nat(a, b))

Uses (7)

Used by (5)