def max_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32.bend:98

import Base
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G

98def max_c(+a: U32, +b: U32, +c: Bool, +hc: {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == c : Bool}) -> {G.pick(U32, c, b, a) == U32.from_nat(Nat.max(U32.to_nat(a), U32.to_nat(b))) : U32}:
99  match c:
100    case True{}:
101      %Equal.sym(Nat, Nat.max(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(b), max_of_lt(U32.to_nat(a), U32.to_nat(b), hc)) : {b == U32.from_nat(_) : U32}
102      Equal.sym(U32, U32.from_nat(U32.to_nat(b)), b, round_trip(b))
103    case False{}:
104      %Equal.sym(Nat, Nat.max(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(a), max_of_ge(U32.to_nat(a), U32.to_nat(b), hc)) : {a == U32.from_nat(_) : U32}
105      Equal.sym(U32, U32.from_nat(U32.to_nat(a)), a, round_trip(a))