def product_double
stelliferous@0.0.2.0 · proofs/binary_division.bend:61
import stelliferous@0.0.2.0/proofs/binary_division.bend as BinaryDivision
import Base
import stelliferous@0.0.2.0/proofs/word_multiplication.bend as Multiplication
61def product_double(+a: Nat,+b: Nat) -> {Nat.mul(Nat.double(a),b) == Nat.double(Nat.mul(a,b)) : Nat}:
62 %Equal.sym(Nat,Nat.mul(Nat.double(a),b),Nat.mul(a,Nat.double(b)),Multiplication.double_mul(a,b)) : {_ == Nat.double(Nat.mul(a,b)) : Nat}
63 product_right(a,b)