def sh_mul

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divd.bend:45

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/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

45# shifting a product shifts one factor
46def sh_mul(+k: Nat, +q: Nat, +b: Nat) -> {C.shift(k, Nat.mul(q, b)) == Nat.mul(C.shift(k, q), b) : Nat}:
47  match k:
48    case 0n:
49      {==}
50    case 1n+ +kp:
51      +i = sh_mul(kp, q, b)
52      +a = Equal.cong(Nat, Nat, w => Nat.double(w), C.shift(kp, Nat.mul(q, b)), Nat.mul(C.shift(kp, q), b), i)
53      +d1 = NA.double_mul(Nat.mul(C.shift(kp, q), b))
54      +d2 = Equal.sym(Nat, Nat.mul(Nat.mul(2n, C.shift(kp, q)), b), Nat.mul(2n, Nat.mul(C.shift(kp, q), b)), NA.mul_assoc(2n, C.shift(kp, q), b))
55      +d3 = Equal.cong(Nat, Nat, w => Nat.mul(w, b), Nat.mul(2n, C.shift(kp, q)), Nat.double(C.shift(kp, q)), Equal.sym(Nat, Nat.double(C.shift(kp, q)), Nat.mul(2n, C.shift(kp, q)), NA.double_mul(C.shift(kp, q))))
56      Equal.trans(Nat, Nat.double(C.shift(kp, Nat.mul(q, b))), Nat.double(Nat.mul(C.shift(kp, q), b)), Nat.mul(Nat.double(C.shift(kp, q)), b), a, Equal.trans(Nat, Nat.double(Nat.mul(C.shift(kp, q), b)), Nat.mul(2n, Nat.mul(C.shift(kp, q), b)), Nat.mul(Nat.double(C.shift(kp, q)), b), d1, Equal.trans(Nat, Nat.mul(2n, Nat.mul(C.shift(kp, q), b)), Nat.mul(Nat.mul(2n, C.shift(kp, q)), b), Nat.mul(Nat.double(C.shift(kp, q)), b), d2, d3)))