def cmul_rel

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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/u64laws.bend as LW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

307def cmul_rel(+q: WU.U64, +x: WU.U64, +n: Nat, +hn: {Nat.mul(v(q), v(x)) == n : Nat}, +c: Bool, +hc: {C.fits(64n, n) == c : Bool}) -> {G.cmul(~WU.U64, ~I.u64_op, ~I.u64_is, q, x) == G.fits(WU.U64, Bool.not(c), of(n)) : Maybe<&2, WU.U64>}:
308  match c:
309    case True{}:
310      +hmo = mo_of(q, x, n, hn, True{}, hc)
311      %Equal.sym(Bool, I.u64_is(NM.MulOver{q, x}), False{}, hmo) : {G.fits(WU.U64, _, I.u64_op(NM.Mul{q, x})) == Some{of(n)} : Maybe<&2, WU.U64>}
312      Equal.cong(WU.U64, Maybe<&2, WU.U64>, t => Some{t}, I.u64_op(NM.Mul{q, x}), of(n), as_of(I.u64_op(NM.Mul{q, x}), n, Equal.trans(Nat, v(I.u64_op(NM.Mul{q, x})), Nat.mul(v(q), v(x)), n, LW.ops_mul(q, x, hmo), hn)))
313    case False{}:
314      %Equal.sym(Bool, I.u64_is(NM.MulOver{q, x}), True{}, mo_of(q, x, n, hn, False{}, hc)) : {G.fits(WU.U64, _, I.u64_op(NM.Mul{q, x})) == None{} : Maybe<&2, WU.U64>}
315      {==}