BinaryDivision.product_double: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/binary_division.bend as BinaryDivision
Lines 61-63 of stelliferous@0.0.2.0/proofs/binary_division.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&start_line=61&end_line=63

import Base
import stelliferous@0.0.2.0/proofs/word_multiplication.bend as Multiplication

def product_double(+a: Nat,+b: Nat) -> {Nat.mul(Nat.double(a),b) == Nat.double(Nat.mul(a,b)) : Nat}:
  %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}
  product_right(a,b)

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&name=product_right
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&name=double_mul