def le

stelliferous@0.0.2.0 · proofs/u32_comparison.bend:100

import Base

100def le(+a: U32,+b: U32) -> {U32.is_le(a,b) == Nat.is_le(U32.to_nat(a),U32.to_nat(b)) : Bool}:
101  %uint(a,b) : {Cmp.is_le(U32.cmp(a,b)) == Cmp.is_le(_) : Bool}
102  {==}