def product_right

stelliferous@0.0.2.0 · proofs/binary_division.bend:51

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

51def product_right(+a: Nat,+b: Nat) -> {Nat.mul(a,Nat.double(b)) == Nat.double(Nat.mul(a,b)) : Nat}:
52  match a:
53    case 0n:
54      {==}
55    case 1n+ +p:
56      %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,
57            b))) : {Nat.add(Nat.double(b),Nat.mul(p,Nat.double(b))) == _ : Nat}
58      %product_right(p,b) : {Nat.add(Nat.double(b),Nat.mul(p,Nat.double(b))) == Nat.add(Nat.double(b),_) : Nat}
59      {==}