def double_mul

stelliferous@0.0.2.0 · proofs/word_multiplication.bend:88

import Base
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition

88def double_mul(+a: Nat,+b: Nat) -> {Nat.mul(Nat.double(a),b) == Nat.mul(a,Nat.double(b)) : Nat}:
89  match a:
90    case 0n:
91      {==}
92    case 1n+ +p:
93      %Addition.double(b) : {Nat.add(b,Nat.add(b,Nat.mul(Nat.double(p),b))) == Nat.add(_,Nat.mul(p,Nat.double(b))) : Nat}
94      %Equal.sym(Nat,Nat.add(Nat.add(b,b),Nat.mul(p,Nat.double(b))),Nat.add(b,Nat.add(b,Nat.mul(p,Nat.double(b)))),Addition.associative(b,b,Nat.mul(p,
95            Nat.double(b)))) : {Nat.add(b,Nat.add(b,Nat.mul(Nat.double(p),b))) == _ : Nat}
96      %double_mul(p,b) : {Nat.add(b,Nat.add(b,Nat.mul(Nat.double(p),b))) == Nat.add(b,Nat.add(b,_)) : Nat}
97      {==}