f は次数,主係数が正の整数係数一変数多項式なら十分ですが,原題の3次式にしました.N は任意の自然数です. let lemma01 = prove (`!x f. f 0 < x /\ (!n. f n < x ==> f (SUC n) < x) ==> !n. f n < x`, REPEAT GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。