def max_ok

lawful-words@0.1.0.0 · proof_u32.bend:962

import Base

962def max_ok(+a: U32, +b: U32, z: Bool, +ez: {U32.is_lt(a, b) == z : Bool}) ->
963  {U32.to_nat(Bool.pick(U32, z, b, a)) == Nat.max(U32.to_nat(a), U32.to_nat(b)) : Nat}:
964  match z:
965    case True{}:
966      Equal.sym(Nat, Nat.max(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(b),
967        max_lt(U32.to_nat(a), U32.to_nat(b), %is_lt_to_nat(a, b) : {_ == True{} : Bool}; ez))
968    case False{}:
969      Equal.sym(Nat, Nat.max(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(a),
970        max_nlt(U32.to_nat(a), U32.to_nat(b), %is_lt_to_nat(a, b) : {_ == False{} : Bool}; ez))