以下は正数である分母 Suc i を払う，両辺から同じものを減ずる，そして，両辺を正数 i で割るといった代数計算です．この種の処理で参照すべき定理は，多くの場合，nat上の性質のreal上への書き換えであり，ここでも thm real_of_nat_Sucreal (Suc ?n) = re…

次は，step ケースです． next case (step i a) 先述の通り，帰納法の変数はi，目標の数列はaとします．証明の流れは，letを用いて，項数がi+1である数列?bを ?b k = a k (k=1,...,i)，GM a 0 i (k=i+1)のように設定，帰納法の仮定 step.IH を適用して，以下…

後半です．statementは lemma amgm_0: fixes a n assumes "0 < n" shows "ALL k. 0 <= a k ==> GM a 0 n <= AM a 0 n" でした．方針は項数がSuc iである任意の数列bでの成立から，項数がiである任意の数列aでの成立を導くというもので，前半は数列を固定し，…