def min_c

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

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

85def min_c(+a: U32, +b: U32, +c: Bool, +hc: {Nat.is_lt(U32.to_nat(b), U32.to_nat(a)) == c : Bool}) -> {G.pick(U32, c, b, a) == U32.from_nat(Nat.min(U32.to_nat(a), U32.to_nat(b))) : U32}:
86  match c:
87    case True{}:
88      %Equal.sym(Nat, Nat.min(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(b), min_of_lt(U32.to_nat(a), U32.to_nat(b), hc)) : {b == U32.from_nat(_) : U32}
89      Equal.sym(U32, U32.from_nat(U32.to_nat(b)), b, round_trip(b))
90    case False{}:
91      %Equal.sym(Nat, Nat.min(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(a), min_of_ge(U32.to_nat(a), U32.to_nat(b), hc)) : {a == U32.from_nat(_) : U32}
92      Equal.sym(U32, U32.from_nat(U32.to_nat(a)), a, round_trip(a))