以上を利用して次に至ります． g`~(?n N. 2 <= n /\ sum(1..n)(\k. &1 / &k) = &N)`;; e(REPEAT STRIP_TAC);; e(MP_TAC (SPEC_ALL floor2) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);; e(MP_TAC (SPEC`xn:num`thm4) THEN ASM_SIMP_TAC[] THEN REPEAT STRI…

同様に第２の和も表せることの証明です．thm8_2はthm7_2を含んだ形になりました． g`!n xn k. n < 2 EXP SUC xn /\ 1 <= xn /\ 2 EXP xn + 1 <= k /\ k <= n ==> ?x y. &2 pow xn / &k = &x / &y /\ EVEN x /\ ODD y`;; e(REPEAT STRIP_TAC);; e(MP_TAC( pro…