def max_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:95

import Base
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as U32P

95def max_c(+a: U32, +b: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{a, b}) == c : Bool}) -> {G.pick(U32, c, b, a) == of(Nat.max(v(a), v(b))) : U32}:
96  match c:
97    case True{}:
98      as_of(b, Nat.max(v(a), v(b)), Equal.sym(Nat, Nat.max(v(a), v(b)), v(b), U32P.max_of_lt(v(a), v(b), lt_of(a, b, True{}, hc))))
99    case False{}:
100      as_of(a, Nat.max(v(a), v(b)), Equal.sym(Nat, Nat.max(v(a), v(b)), v(a), U32P.max_of_ge(v(a), v(b), lt_of(a, b, False{}, hc))))