law u32_cmp_refl_sym

bend-mathlib@0.8.1.0 · string.bend:593

import Base

593# Comparing a U32 with itself gives EQ, reversed to rewrite toward the simple side.
594law u32_cmp_refl_sym:
595  for x: U32
596  {EQ{} == U32.cmp(x, x) : Cmp}