def even_total

stelliferous@0.0.2.0 · proofs/binary_division.bend:65

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

65def even_total(+q: Nat,+r: Nat,+b: Nat) -> {Nat.add(Nat.mul(Nat.double(q),b),Nat.double(r)) == Nat.double(Nat.add(Nat.mul(q,b),r)) : Nat}:
66  %Equal.sym(Nat,Nat.mul(Nat.double(q),b),Nat.double(Nat.mul(q,b)),product_double(q,b)) : {Nat.add(_,
67      Nat.double(r)) == Nat.double(Nat.add(Nat.mul(q,b),r)) : Nat}
68  Equal.sym(Nat,Nat.double(Nat.add(Nat.mul(q,b),r)),Nat.add(Nat.double(Nat.mul(q,b)),Nat.double(r)),WordEncoding.double_add(Nat.mul(q,b),r))