def min_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:87

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
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

87def min_c(+a: WU.U64, +b: WU.U64, +c: Bool, +hc: {I.u64_is(NM.Lt{b, a}) == c : Bool}) -> {G.pick(WU.U64, c, b, a) == of(Nat.min(v(a), v(b))) : WU.U64}:
88  match c:
89    case True{}:
90      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))))
91    case False{}:
92      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))))