原です。

In [ruby-math:00955] 

>正木です。
>
>In [ruby-math:00948]
>
>|原です。
>
>|ちょっと証明の補強します。プログラムでは

>少なくとも a, b, c が正のときは
>
>(a.div(b)).div(c) == a.div(b * c)
>
>なのでまったく問題が無いのでは？

その通りです。混乱させてしまってすいません。正木さんの 
[ruby-math:00945] の証明は完全でした。なんと私はその公式に気づい
ていなかったのです。私の証明は別証に過ぎませんでした。


公式の証明をしておきますね。次は補題と呼ぶにも大げさですが、

【補題】A, B, C(>0) を整数とすると「A/C < B ならば (A + 1)/C <= B.」

さて、一般の x について次が言えます。

【命題】n を自然数とすると [[x]/n] = [x/n]。

（証明）[x]/n < [[x]/n] + 1 に【補題】を適用して 
([x] + 1)/n <= [[x]/n] + 1. x/n < 左辺、より x/n < [[x]/n] + 1. 
x/n >= [[x]/n] の方は明らかだから、 [[x]/n] = [x/n].
 
ここで x = a/b, n = c として当てはめると、

【系】c が自然数なら a.div(b).div(c) == a.div(b*c).

ちなみに、[[3/2]/1.5] = 0、 [3/(2*1.5)] = 1 なので、c が自然数で
あるという条件ははずせません。

うーん、今まで知らなかったとは、、、内緒にしておいてください。
(^^;


次は、近岡さんの [ruby-math:00947] の別証です。帰納法の仮定を
 |(x/k - sqrt([a/k**2])| < 1 から |x/k - sqrt(a/k**2)| < 1 へ
変更してシンプルにしただけです。

【定理】x, k を自然数で 2|k|x, k**4 <= 4*a とするとき、

        N(x) = [(x + [a/x])/2]

    に対し次が成り立つ。

        |x/k - sqrt(a)/k| < 1 ならば |N(x) - sqrt(a)| < 1.

（証明）y = (x**2 + a)/(2*x) とおくと上の【系】から N(x) = [y] で
ある。また、仮定より

  y - sqrt(a) = (x - sqrt(a))**2/(2*x) < k**2/(2*x).

一方、k**4 <= 4*a より k/2 <= sqrt(a)/k. 
再び仮定より、sqrt(a)/k < x/k + 1 なので k/2 < x/k + 1. 
両辺は整数だから、k/2 <= x/k. よって k**2/(2*x) <= 1. 
以上より y - sqrt(a) < 1.
y の整数部分をとって -1 < N(x) - sqrt(a) < 1.