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 even
open import nat
open import logic

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

open _∧_

open import prime

-- equlid : ( n m k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * m ) → Dividable k n ∨ Dividable k m
-- equlid = {!!}

divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n
divdable^2 zero zero () 1<n pk dn2
divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
... | yes y = y
... | no non with gcd-euclid (suc k) (suc n) (suc n) 1<k (<-trans a<sa 1<n) (<-trans a<sa 1<n) (Prime.isPrime pk) dn2 
... | case1 dn = dn
... | case2 dm = dm

-- gcd-div : ( i j k : ℕ ) → (if : Dividable k i) (jf : Dividable k j )
--    → Dividable k ( gcd i  j )

root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime (suc p) → m > 1  →  (suc p) * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
root-prime-irrational n m p n>1 pn m>1 pnm = rot13 ( gcd-div n m (suc p) 1<sp dn dm ) where 
    1<sp : 1 < suc p
    1<sp = Prime.p>1 pn
    rot13 : {m : ℕ } → Dividable (suc p) m →  m ≡ 1 → ⊥
    rot13 d refl with Dividable.factor d | Dividable.is-factor d
    ... | zero | ()   -- gcd 0 m ≡ 1
    ... | suc n | x = ⊥-elim ( nat-≡< (sym x) rot17 ) where -- x : (suc n * suc p + 0) ≡ 1 
        rot17 : suc n * suc p + 0 > 1
        rot17 = begin
           2 ≡⟨ refl ⟩
           suc (1 * 1 )  ≤⟨ {!!}  ⟩
           suc (1 * suc p )  <⟨ {!!}  ⟩
           suc (0 + n * suc p )  ≤⟨ {!!}  ⟩
           suc (p + n * suc p )  ≡⟨ +-comm 0 _ ⟩
           suc n * suc p + 0 ∎   where open ≤-Reasoning
    dm : Dividable (suc p) m
    dm = divdable^2 m (suc p) 1<sp m>1 pn record { factor = n * n ; is-factor = begin
       (n * n) * (suc p) + 0 ≡⟨  +-comm _ 0 ⟩
       (n * n) * (suc p)  ≡⟨ *-comm (n * n) (suc p) ⟩
       (suc p) * (n * n)  ≡⟨ sym (*-assoc (suc p) n n)  ⟩
       (suc p * n) * n ≡⟨ pnm ⟩
       m * m ∎ }  where open ≡-Reasoning
     -- (suc p) * n * n = 2m' 2m'
     --  n * n = m' 2m'
    df = Dividable.factor dm
    dn : Dividable (suc p) n
    dn = divdable^2 n (suc p) 1<sp n>1 pn record { factor = df * df  ; is-factor = begin
        df * df * (suc p) + 0  ≡⟨ *-cancelʳ-≡ _ _ {p} ( begin 
          (df * df * (suc p) + 0) * (suc p) ≡⟨  cong (λ k → k * (suc p))  (+-comm (df * df * (suc p)) 0)  ⟩
          ((df * df) * (suc p)) * (suc p) ≡⟨ cong (λ k → k * (suc p)) (*-assoc df df (suc p) ) ⟩
          (df * (df * (suc p))) * (suc p) ≡⟨ cong (λ k → (df * k ) * (suc p)) (*-comm df (suc p))  ⟩
          (df * ((suc p) * df)) * (suc p) ≡⟨ sym ( cong (λ k → k * (suc p)) (*-assoc df (suc p) df ) ) ⟩
          ((df * (suc p)) * df) * (suc p) ≡⟨ *-assoc (df * (suc p)) df (suc p)  ⟩
          (df * (suc p)) * (df * (suc p)) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * (suc p))) (+-comm 0 _) ⟩
          (df * (suc p) + 0) * (df * (suc p) + 0)   ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩
          m * m   ≡⟨ sym pnm ⟩
          (suc p) * n * n   ≡⟨ cong (λ k → k * n) (*-comm (suc p) n) ⟩
          n * (suc p) * n   ≡⟨ *-assoc n (suc p) n ⟩
          n * (suc p * n)   ≡⟨ cong (λ k → n * k) (*-comm (suc p) n) ⟩
          n * (n * suc p)   ≡⟨ sym (*-assoc n n (suc p)) ⟩
          n * n * (suc p) ∎  ) ⟩
       n * n ∎ }  where open ≡-Reasoning