√２が無理数であること

theorem sqrt_two_irrational {a b : ℕ}
    (co : gcd a b = 1) : a^2 ≠ 2 * b^2

証明の方針

1. 証明したい主張が間違っている（-i.e. `a^2 = 2 * b^2`）と仮定

2. 仮定から `1=2` を示す

3. `1=2` が偽であるので主張が正しい（-i.e. `a^2 ≠ 2 * b^2`）ことが示される