sqrt2.tex

\documentclass[12pt]{article}
\usepackage[a4paper]{geometry}
\geometry{verbose,tmargin=2cm,bmargin=2cm,lmargin=2cm,rmargin=2cm}
\usepackage[T2A]{fontenc}
\usepackage[english,russian]{babel}
\usepackage{amsmath, amsthm, amssymb, amsfonts}
\begin{document}
Доказательство иррациональности $\sqrt{2}$ дано еще в Началах Евклида.

Доказывается от противного: предположим, что $\sqrt{2} = \frac{p}{q}$, где $\frac{p}{q}$ --- несократимая дробь, делаем выводы:

$$
\sqrt{2} = \frac{p}{q} \implies 2 = \left(\frac{p}{q}\right)^2 \implies p^2 = 2 \cdot q^2
$$

Здесь нужна лемма: ``Если квадрат числа четный, то число тоже четно''. Из этого делаем вывод, что т.к. квадрат p --- четный, то p --- тоже четно. Пусть $p = 2 \cdot m$:

$$
(2 \cdot m)^2 = 2 \cdot q^2 \implies 4 \cdot m^2 = 2 \cdot q^2 \implies 2 \cdot m^2 = q^2
$$

Из леммы ``Если квадрат числа четный, то число тоже четно'' следует, что q --- четное число. Пусть $q = 2 \cdot n$. Тогда мы получаем, что:

$$
\frac{p}{q} = \frac{2 \cdot m}{2 \cdot n} = \frac{m}{n}
$$

Но по условию $\frac{p}{q}$ --- несократимая дробь, а мы доказали, что её можно сократить на 2. Мы пришли к противоречию, следовательно наше предположение не верно, и $\sqrt{2}$ не может быть представлен в виде несократимой дроби вида $\frac{p}{q}$.

Для доказательства в coq нам понадобятся рациональные числа, лемма про четность: если квадрат числа четный, то и число четно. Как-то описать условие несократимости дроби.

При доказательстве от противного мы должны получить False в контексте.
\end{document}