Coq in a Hurryの練習問題の一番最後。 とすると であるから、となる正の整数の組のなかで、最小のをとってくる。 すると、であるから。これは矛盾であり2の平方根が有理数でないことの証明になっている。 この証明をCoqを使って書け。 これはとてつもなく…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。