def min_c

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

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

85def min_c(+a: U32, +b: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{b, a}) == c : Bool}) -> {G.pick(U32, c, b, a) == of(Nat.min(v(a), v(b))) : U32}:
86  match c:
87    case True{}:
88      as_of(b, Nat.min(v(a), v(b)), Equal.sym(Nat, Nat.min(v(a), v(b)), v(b), U32P.min_of_lt(v(a), v(b), lt_of(b, a, True{}, hc))))
89    case False{}:
90      as_of(a, Nat.min(v(a), v(b)), Equal.sym(Nat, Nat.min(v(a), v(b)), v(a), U32P.min_of_ge(v(a), v(b), lt_of(b, a, False{}, hc))))