def dbl_mul

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/width.bend:358

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

358def dbl_mul(+x: Nat, +y: Nat) -> {Nat.double(Nat.mul(x, y)) == Nat.mul(x, Nat.double(y)) : Nat}:
359  Equal.trans(Nat, Nat.double(Nat.mul(x, y)), Nat.add(Nat.mul(x, y), Nat.mul(x, y)), Nat.mul(x, Nat.double(y)), NA.double_self(Nat.mul(x, y)), Equal.trans(Nat, Nat.add(Nat.mul(x, y), Nat.mul(x, y)), Nat.mul(x, Nat.add(y, y)), Nat.mul(x, Nat.double(y)), Equal.sym(Nat, Nat.mul(x, Nat.add(y, y)), Nat.add(Nat.mul(x, y), Nat.mul(x, y)), NA.mul_add_left(x, y, y)), Equal.cong(Nat, Nat, t => Nat.mul(x, t), Nat.add(y, y), Nat.double(y), Equal.sym(Nat, Nat.double(y), Nat.add(y, y), NA.double_self(y)))))