def ge_true

stelliferous@0.0.2.0 · proofs/nat_order.bend:236

import Base

236def ge_true(+a: Nat,+b: Nat,h: {Nat.is_ge(a,b) == True{} : Bool}) -> {Nat.is_le(b,a) == True{} : Bool}:
237  %ge_le(a,b) : {_ == True{} : Bool}
238  h