def fin2

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
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/natural.bend as M
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I

588def fin2(+m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +s: U32, +sn: Nat, +hs: {v(s) == sn : Nat}, +cb: Bool, +gn: Nat, +hcb: {Bool.and(Bool.not(Nat.is_lt(gn, 1n)), Bool.not(Nat.is_lt(1n, gn))) == cb : Bool}) -> {G.inv_one(~U32, ~I.u32_op, m, s, cb) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, M.BZ{gn, sn})) : Result<&2, &2, NM.NumError, U32>}:
589  match cb gn:
590    case True{} 1n:
591      Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.Rem{s, m}), of(Nat.mod(sn, 1n+mp)), as_of(I.u32_op(NM.Rem{s, m}), Nat.mod(sn, 1n+mp), Equal.trans(Nat, v(I.u32_op(NM.Rem{s, m})), Nat.mod(v(s), 1n+mp), Nat.mod(sn, 1n+mp), pm_rem(s, m, mp, hm), Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+mp), v(s), sn, hs))))
592    case False{} 1n:
593      Empty.absurd({G.inv_one(~U32, ~I.u32_op, m, s, False{}) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, M.BZ{1n, sn})) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(hcb))
594    case True{} 0n:
595      Empty.absurd({G.inv_one(~U32, ~I.u32_op, m, s, True{}) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, M.BZ{0n, sn})) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hcb)))
596    case False{} 0n:
597      {==}
598    case True{} 2n+h:
599      Empty.absurd({G.inv_one(~U32, ~I.u32_op, m, s, True{}) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, M.BZ{2n+h, sn})) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hcb)))
600    case False{} 2n+h:
601      {==}