law cmp_to_nat

lawful-words@0.1.0.0 · proof_u32.bend:220

import Base

220law cmp_to_nat:
221  for +a: U32
222  for +b: U32
223  {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}