the division algorithm.txt

s / t
  where t ≠ 0

s / t = As / At
  where 1 / 2 <= At < 1

As / At = As / {1-(1-At)}
  ∴ 0 < (1-At) <= 1 / 2

As / {1-(1-At)} = As*{1+(1-At)} / {1-(1-At)^2}
  ∴ 0 < (1-At)^2 <= 1 / 4

As*{1+(1-At)} / {1-(1-At)^2} = As*{1+(1-At)}*{1+(1-At)^2} / {1-(1-At)^4}
  ∴ 0 < (1-At)^4 <= 1 / 16

∴ s / t = As / At = As*Π_{k∈[0, n)}{1+(1-At)^2^k} / {1-(1-At)^2^n}
  ∴ 0 < (1-At)^2^n <= (1 / 2)^2^n

∴ s / t = lim_{n → ∞} As*Π_{k∈[0, n)}{1+(1-At)^2^k} / {1-(1-At)^2^n} = As*Π_{k∈[0, ∞)}{1+(1-At)^2^k}
  where 0 < s / t - As*Π_{k∈[0, n)}{1+(1-At)^2^k} = {(1-At)^2^n}*s / t  <= {(1 / 2)^2^n}*s / t = s / (2^2^n)*t