BinaryDivision.product_right: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/binary_division.bend as BinaryDivision
Lines 51-59 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=51&end_line=59

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

def product_right(+a: Nat,+b: Nat) -> {Nat.mul(a,Nat.double(b)) == Nat.double(Nat.mul(a,b)) : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+ +p:
      %Equal.sym(Nat,Nat.double(Nat.add(b,Nat.mul(p,b))),Nat.add(Nat.double(b),Nat.double(Nat.mul(p,b))),WordEncoding.double_add(b,Nat.mul(p,
            b))) : {Nat.add(Nat.double(b),Nat.mul(p,Nat.double(b))) == _ : Nat}
      %product_right(p,b) : {Nat.add(Nat.double(b),Nat.mul(p,Nat.double(b))) == Nat.add(Nat.double(b),_) : Nat}
      {==}

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.add
  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/word_encoding.bend&name=double_add