def ge

stelliferous@0.0.2.0 · proofs/u32_comparison.bend:108

import Base

108def ge(+a: U32,+b: U32) -> {U32.is_ge(a,b) == Nat.is_ge(U32.to_nat(a),U32.to_nat(b)) : Bool}:
109  %uint(a,b) : {Cmp.is_ge(U32.cmp(a,b)) == Cmp.is_ge(_) : Bool}
110  {==}