def max_val_c

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

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

156def max_val_c(+x: U32, +lo: U32, +c: Bool, +hc: {Nat.is_lt(U32.to_nat(x), U32.to_nat(lo)) == c : Bool}) -> {U32.to_nat(G.pick(U32, c, lo, x)) == Nat.max(U32.to_nat(x), U32.to_nat(lo)) : Nat}:
157  match c:
158    case True{}:
159      Equal.sym(Nat, Nat.max(U32.to_nat(x), U32.to_nat(lo)), U32.to_nat(lo), max_of_lt(U32.to_nat(x), U32.to_nat(lo), hc))
160    case False{}:
161      Equal.sym(Nat, Nat.max(U32.to_nat(x), U32.to_nat(lo)), U32.to_nat(x), max_of_ge(U32.to_nat(x), U32.to_nat(lo), hc))