module root2 where

open import Data.Nat 
open import Data.Nat.Properties
open import Data.Empty
open import Data.Unit using (⊤ ; tt)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions

open import gcd
open import nat

record Rational : Set where
  field
    i j : ℕ
    coprime : gcd i j ≡ 1

root2-irrational : ( n m : ℕ ) → n > 1 → m > 1  →  2 * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
root2-irrational n m n>1 m>1 2nm = gcd24 {n} {m} n>1 m>1 (s≤s (s≤s z≤n)) (even→gcd=2 rot7 (rot5 n>1)) (even→gcd=2 ( even^2 {m} ( rot1)) (rot5 m>1))where
    rot5 : {n : ℕ} → n > 1 → n > 0
    rot5 {n} lt = <-trans a<sa lt 
    rot1 : even ( m * m )
    rot1 = subst (λ k → even k ) rot4 (n*even {n * n} {2} tt ) where
       rot4 : (n * n) * 2 ≡ m * m  
       rot4 = begin
          (n * n) * 2     ≡⟨ *-comm (n * n) 2 ⟩
          2 * ( n * n )   ≡⟨ sym (*-assoc 2 n n) ⟩
          2 *  n * n      ≡⟨ 2nm ⟩
          m * m           ∎ where open ≡-Reasoning
    E : Even m
    E = e2 m ( even^2 {m} ( rot1 ))
    rot2 : 2 * n * n ≡ 2 * Even.j E * m
    rot2 = subst (λ k → 2 * n * n ≡ k * m ) (Even.is-twice E) 2nm
    rot3 : n * n ≡ Even.j E * m
    rot3 = e3 ( begin
          2 * (n * n)   ≡⟨ sym (*-assoc 2 n _) ⟩
          2 *  n * n    ≡⟨ rot2 ⟩
          2 * Even.j E * m ≡⟨  *-assoc 2 (Even.j E)  m  ⟩
          2 * (Even.j E * m)  ∎ ) where open ≡-Reasoning
    rot7 : even n  
    rot7 =  even^2 {n} (subst (λ k → even k) (sym rot3) ((n*even {Even.j E} {m} ( even^2 {m} ( rot1 )))))