def min_ok

lawful-words@0.1.0.0 · proof_u32.bend:952

import Base

952def min_ok(+a: U32, +b: U32, z: Bool, +ez: {U32.is_lt(a, b) == z : Bool}) ->
953  {U32.to_nat(Bool.pick(U32, z, a, b)) == Nat.min(U32.to_nat(a), U32.to_nat(b)) : Nat}:
954  match z:
955    case True{}:
956      Equal.sym(Nat, Nat.min(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(a),
957        min_lt(U32.to_nat(a), U32.to_nat(b), %is_lt_to_nat(a, b) : {_ == True{} : Bool}; ez))
958    case False{}:
959      Equal.sym(Nat, Nat.min(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(b),
960        min_nlt(U32.to_nat(a), U32.to_nat(b), %is_lt_to_nat(a, b) : {_ == False{} : Bool}; ez))