module root2 where

open import Data.Nat
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Nat.DivMod

even : (n : ℕ ) → Set
even n =  n % 2 ≡ 0 

even? : (n : ℕ ) → Dec ( even n )
even? n with n % 2
even? n | zero = yes refl
even? n | suc k = no ( λ () )

nn-even : {n : ℕ } → even n → even ( n * n )
nn-even {n} eq = {!!}

2-even : {n : ℕ } → even ( 2 * n )
2-even {n} = {!!}

even-2 : (n : ℕ ) → (n + 2) % 2 ≡ 0 → n % 2 ≡ 0 
even-2 0 refl = refl
even-2 1 () 
even-2 (suc (suc n)) eq = {!!} -- trans ([a+n]%n≡a%n (suc (suc n)) _ ) eq -- [a+n]%n≡a%n : ∀ a n → (a + suc n) % suc n ≡ a % suc n

even-half : (n : ℕ ) → even n → ℕ 
even-half zero _ = zero
even-half (suc (suc n)) ev = {!!} -- 1 + even-half n (subst (λ k → k ≡ 0 ) {!!} {!!} )

root2-irrational : ( n m : ℕ ) → ¬ ( 2 * n * n ≡ m * m )
root2-irrational n m eq = {!!}