def fv_mul

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

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/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

963def fv_mul(+a: WU.U64, +x: WU.U64, +n: Nat, +hn: {Nat.mul(v(a), v(x)) == n : Nat}, +c: Bool, +hc: {C.fits(64n, n) == c : Bool}) -> {fv(Bool.not(I.u64_is(NM.MulOver{a, x})), v(I.u64_op(NM.Mul{a, x})), n) == n : Nat}:
964  match c:
965    case True{}:
966      +hmo = mo_of(a, x, n, hn, True{}, hc)
967      %Equal.sym(Bool, I.u64_is(NM.MulOver{a, x}), False{}, hmo) : {fv(Bool.not(_), v(I.u64_op(NM.Mul{a, x})), n) == n : Nat}
968      Equal.trans(Nat, v(I.u64_op(NM.Mul{a, x})), Nat.mul(v(a), v(x)), n, LW.ops_mul(a, x, hmo), hn)
969    case False{}:
970      %Equal.sym(Bool, I.u64_is(NM.MulOver{a, x}), True{}, mo_of(a, x, n, hn, False{}, hc)) : {fv(Bool.not(_), v(I.u64_op(NM.Mul{a, x})), n) == n : Nat}
971      {==}