def digit_total

stelliferous@0.0.2.0 · proofs/binary_division.bend:70

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

70def digit_total(+bit: Bool,+q: Nat,+r: Nat,+b: Nat) -> {Nat.add(Nat.mul(Nat.double(q),b),Comparison.digit(bit,r)) == Comparison.digit(bit,
71    Nat.add(Nat.mul(q,b),r)) : Nat}:
72  match bit:
73    case False{}:
74      even_total(q,r,b)
75    case True{}:
76      %Equal.sym(Nat,Nat.add(Nat.mul(Nat.double(q),b),1n+Nat.double(r)),1n+Nat.add(Nat.mul(Nat.double(q),b),Nat.double(r)),
77        Addition.successor_right(Nat.mul(Nat.double(q),b),Nat.double(r))) : {_ == 1n+Nat.double(Nat.add(Nat.mul(q,b),r)) : Nat}
78      %even_total(q,r,b) : {1n+Nat.add(Nat.mul(Nat.double(q),b),Nat.double(r)) == 1n+_ : Nat}
79      {==}