それでは２のべき乗の場合を証明していきます．lemmaの名前とstatementは lemma amgm_2: fixes a m n shows "ALL k. 0 <= a k ==> GM a m (2 ^ n) <= AM a m (2 ^ n)" 証明は項数についての帰納法ですが，数列はaとして固定し，その隣接する任意の2^N項につ…

これで記号の準備が出来ました．証明は項数についての帰納法，すなわち，２の累乗の場合をまず示し，それを元に，Suc n から n への（見かけ上）後ろ向きの帰納法で隙間を埋めます． まず，それぞれのstatementを書いてみます． lemma amgm_2: fixes a m n s…