def fin2

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

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

589def fin2(+m: WU.U64, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +s: WU.U64, +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(~WU.U64, ~I.u64_op, m, s, cb) == SG.lift(~WU.U64, ~SG.u64_of, M.inv_fin(1n+mp, M.BZ{gn, sn})) : Result<&2, &2, NM.NumError, WU.U64>}:
590  match cb gn:
591    case True{} 1n:
592      Equal.cong(WU.U64, Result<&2, &2, NM.NumError, WU.U64>, t => Done{t}, I.u64_op(NM.Rem{s, m}), of(Nat.mod(sn, 1n+mp)), as_of(I.u64_op(NM.Rem{s, m}), Nat.mod(sn, 1n+mp), Equal.trans(Nat, v(I.u64_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))))
593    case False{} 1n:
594      Empty.absurd({G.inv_one(~WU.U64, ~I.u64_op, m, s, False{}) == SG.lift(~WU.U64, ~SG.u64_of, M.inv_fin(1n+mp, M.BZ{1n, sn})) : Result<&2, &2, NM.NumError, WU.U64>}, true_ne_false(hcb))
595    case True{} 0n:
596      Empty.absurd({G.inv_one(~WU.U64, ~I.u64_op, m, s, True{}) == SG.lift(~WU.U64, ~SG.u64_of, M.inv_fin(1n+mp, M.BZ{0n, sn})) : Result<&2, &2, NM.NumError, WU.U64>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hcb)))
597    case False{} 0n:
598      {==}
599    case True{} 2n+h:
600      Empty.absurd({G.inv_one(~WU.U64, ~I.u64_op, m, s, True{}) == SG.lift(~WU.U64, ~SG.u64_of, M.inv_fin(1n+mp, M.BZ{2n+h, sn})) : Result<&2, &2, NM.NumError, WU.U64>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hcb)))
601    case False{} 2n+h:
602      {==}