{-# OPTIONS --allow-unsolved-metas #-}
module gcd 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 nat
open import logic

record Factor (n m : ℕ ) : Set where
   field 
      factor : ℕ
      remain : ℕ
      is-factor : factor * n + remain ≡ m

record Dividable (n m : ℕ ) : Set where
   field 
      factor : ℕ
      is-factor : factor * n + 0 ≡ m 

open Factor

DtoF : {n m : ℕ} → Dividable n m → Factor n m
DtoF {n} {m} record { factor = f ; is-factor = fa } = record { factor = f ; remain = 0 ; is-factor = fa }

FtoD : {n m : ℕ} → (fc : Factor n m) → remain fc ≡ 0 → Dividable n m 
FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } refl = record { factor = f ; is-factor = fa }

--decD : {n m : ℕ} → Dec (Dividable n m)
--decD = {!!}

--divdable^2 : ( n k : ℕ ) → Dividable k ( n * n ) → Dividable k n
--divdable^2 n k dn2 = {!!}

decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = 
 decf1 {n} {k} f r fa where
  decf1 : { n k : ℕ } → (f r : ℕ) → (f * k + r ≡ suc n)  → Factor k n 
  decf1 {n} {k} f (suc r) fa  =  -- this case must be the first
     record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n
        f * k + r ≡⟨ cong pred ( begin
          suc ( f * k + r ) ≡⟨ +-comm _ r ⟩
          r + suc (f * k)  ≡⟨ sym (+-assoc r 1 _) ⟩
          (r + 1) + f * k ≡⟨ cong (λ t → t + f * k ) (+-comm r 1) ⟩
          (suc r ) + f * k ≡⟨ +-comm (suc r) _ ⟩
          f * k + suc r  ≡⟨ fa ⟩
          suc n ∎ ) ⟩ 
        n ∎ ) }  where open ≡-Reasoning
  decf1 {n} {zero} (suc f) zero fa  = ⊥-elim ( nat-≡< fa (
        begin suc (suc f * zero + zero) ≡⟨ cong suc (+-comm _ zero)  ⟩
        suc (f * 0) ≡⟨ cong suc (*-comm f zero)  ⟩
        suc zero ≤⟨ s≤s z≤n ⟩
        suc n ∎ )) where open ≤-Reasoning
  decf1 {n} {suc k} (suc f) zero fa  = 
     record { factor = f ; remain = k ; is-factor = ( begin -- fa : suc (k + f * suc k + zero) ≡ suc n
        f * suc k + k ≡⟨ +-comm _ k ⟩
        k + f * suc k ≡⟨ +-comm zero _ ⟩
        (k + f * suc k) + zero  ≡⟨ cong pred fa ⟩
        n ∎ ) }  where open ≡-Reasoning

div0 :  {k : ℕ} → Dividable k 0
div0 {k} = record { factor = 0; is-factor = refl }

div= :  {k : ℕ} → Dividable k k
div= {k} = record { factor = 1; is-factor = ( begin
        k + 0 * k + 0  ≡⟨ trans ( +-comm _ 0) ( +-comm _ 0) ⟩
        k ∎ ) }  where open ≡-Reasoning

gcd1 : ( i i0 j j0 : ℕ ) → ℕ
gcd1 zero i0 zero j0 with <-cmp i0 j0
... | tri< a ¬b ¬c = i0
... | tri≈ ¬a refl ¬c = i0
... | tri> ¬a ¬b c = j0
gcd1 zero i0 (suc zero) j0 = 1
gcd1 zero zero (suc (suc j)) j0 = j0
gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
gcd1 (suc zero) i0 zero j0 = 1
gcd1 (suc (suc i)) i0 zero zero = i0
gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i))  j0 (suc j0)
gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0  

gcd : ( i j : ℕ ) → ℕ
gcd i j = gcd1 i i j j 

gcd20 : (i : ℕ) → gcd i 0 ≡ i
gcd20 zero = refl
gcd20 (suc i) = gcd201 (suc i) where
    gcd201 : (i : ℕ ) → gcd1 i i zero zero ≡ i
    gcd201 zero = refl
    gcd201 (suc zero) = refl
    gcd201 (suc (suc i)) = refl

gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
gcd22 zero i0 zero o0 = refl
gcd22 zero i0 (suc o) o0 = refl
gcd22 (suc i) i0 zero o0 = refl
gcd22 (suc i) i0 (suc o) o0 = refl 

gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m
gcdmm zero m with <-cmp m m
... | tri< a ¬b ¬c = refl
... | tri≈ ¬a refl ¬c = refl
... | tri> ¬a ¬b c = refl
gcdmm (suc n) m  = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m )

gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i
gcdsym2 i j with <-cmp i j | <-cmp j i
... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) 
... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 
... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 
... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) 
... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) 
... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) 
gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0
gcdsym1 zero zero zero zero = refl
gcdsym1 zero zero zero (suc j0) = refl
gcdsym1 zero (suc i0) zero zero = refl
gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0)
gcdsym1 zero zero (suc zero) j0 = refl
gcdsym1 zero zero (suc (suc j)) j0 = refl
gcdsym1 zero (suc i0) (suc zero) j0 = refl
gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j))
gcdsym1 (suc zero) i0 zero j0 = refl
gcdsym1 (suc (suc i)) i0 zero zero = refl
gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0) 
gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 )

gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n
gcdsym {n} {m} = gcdsym1 n n m m 

gcd11 : ( i  : ℕ ) → gcd i i ≡ i
gcd11 i = gcdmm i i 


gcd203 : (i : ℕ) → gcd1 (suc i) (suc i) i i ≡ 1
gcd203 zero = refl
gcd203 (suc i) = gcd205 (suc i) where
   gcd205 : (j : ℕ) → gcd1 (suc j) (suc (suc i)) j (suc i) ≡ 1
   gcd205 zero = refl
   gcd205 (suc j) = subst (λ k → k ≡ 1) (gcd22 (suc j)  (suc (suc i)) j (suc i)) (gcd205 j)

gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1
gcd204 zero = refl
gcd204 (suc zero) = refl
gcd204 (suc (suc zero)) = refl
gcd204 (suc (suc (suc i))) = gcd204 (suc (suc i)) 

gcd+j : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j
gcd+j i j = gcd200 i i j j refl refl where
       gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1)
       gcd202 zero j1 = refl
       gcd202 (suc i) j1 = cong suc (gcd202 i j1)
       gcd201 : (i i0 j j0 j1 : ℕ) → gcd1 (i + j1) (i0 + suc j) j1 j0 ≡ gcd1 i (i0 + suc j) zero j0
       gcd201 i i0 j j0 zero = subst (λ k → gcd1 k (i0 + suc j) zero j0 ≡ gcd1 i (i0 + suc j) zero j0 ) (+-comm zero i) refl
       gcd201 i i0 j j0 (suc j1) = begin
          gcd1 (i + suc j1)   (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩
          gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩
          gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩
          gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning
       gcd200 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0
       gcd200 i .i zero .0 refl refl = subst (λ k → gcd1 k k zero zero ≡ gcd1 i i zero zero ) (+-comm zero i) refl 
       gcd200 (suc (suc i)) i0 (suc j) (suc j0) i=i0 j=j0 = gcd201 (suc (suc i)) i0 j (suc j0) (suc j)
       gcd200 zero zero (suc zero) .1 i=i0 refl = refl
       gcd200 zero zero (suc (suc j)) .(suc (suc j)) i=i0 refl = begin
          gcd1 (zero + suc (suc j)) (zero + suc (suc j)) (suc (suc j)) (suc (suc j)) ≡⟨ gcdmm (suc (suc j)) (suc (suc j)) ⟩
          suc (suc j) ≡⟨ sym (gcd20 (suc (suc j))) ⟩
          gcd1 zero zero (suc (suc j)) (suc (suc j)) ∎ where open ≡-Reasoning
       gcd200 zero (suc i0) (suc j) .(suc j) () refl
       gcd200 (suc zero) .1 (suc j) .(suc j) refl refl = begin
          gcd1 (1 + suc j) (1 + suc j) (suc j) (suc j) ≡⟨ gcd203 (suc j) ⟩
          1 ≡⟨ sym ( gcd204 (suc j)) ⟩
          gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning
       gcd200 (suc (suc i)) i0 (suc j) zero i=i0 ()

div1 : { k : ℕ } → k > 1 →  ¬  Dividable k 1
div1 {k} k>1 record { factor = (suc f) ; is-factor = fa } = ⊥-elim ( nat-≡< (sym fa) ( begin
    2 ≤⟨ k>1 ⟩
    k ≡⟨ +-comm 0 _ ⟩
    k + 0 ≡⟨ refl  ⟩
    1 * k ≤⟨ *-mono-≤ {1} {suc f} (s≤s z≤n ) ≤-refl ⟩
    suc f * k ≡⟨ +-comm 0 _ ⟩
    suc f * k + 0 ∎  )) where open ≤-Reasoning  

div-div : { i j k : ℕ } → k > 1 →  Dividable k i →  Dividable k j → Dividable k (i - j) ∧ Dividable k (j - i)
div-div {i} {j} {suc k} k>1 di dj = div-div0 di dj where
   div-div1 : {i j : ℕ}   →  Dividable (suc k) i →  Dividable (suc k) j → i < j  → Dividable (suc k) (j - i)
   div-div1 {i} {j} record { factor = fi ; is-factor = fai } record { factor = fj ; is-factor = faj } i<j =
            subst (λ g →  Dividable (suc k) g ) div-div3 ( div-div2 fj fi fi<fj ) where
      fi<fj : fi < fj
      fi<fj with <-cmp fi fj
      ... | tri< a ¬b ¬c = a
      ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (cong (λ g → g * suc k + 0) b) (begin
             suc (fi * suc k + 0)  ≡⟨ cong suc fai ⟩
             suc i  ≤⟨ i<j ⟩
             j  ≡⟨ sym faj ⟩
             fj * suc k + 0 ∎  )) where open ≤-Reasoning  
      ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> (*-monoˡ-< k c ) (begin
             suc (fi * suc k) ≡⟨ +-comm 0 _ ⟩
             suc (fi * suc k + 0) ≡⟨ cong suc fai ⟩
             suc i ≤⟨ i<j ⟩
             j ≡⟨ sym faj ⟩
             fj * suc k + 0 ≡⟨ +-comm _ 0 ⟩
             fj * suc k ∎  )) where open ≤-Reasoning  
      div-div3 : (fj * suc k) - (fi * suc k) ≡ j - i
      div-div3 = begin (fj * suc k) - (fi * suc k) ≡⟨  cong₂ (λ g h → g - h) (+-comm 0 (fj * suc k)) (+-comm 0 (fi * suc k)) ⟩
          (fj * suc k + 0) - (fi * suc k + 0) ≡⟨  cong₂ (λ g h → g - h) faj  fai ⟩
          j - i ∎  where open ≡-Reasoning  
      div-div2 : (fj fi : ℕ) → fi < fj → Dividable (suc k) ((fj * suc k) - (fi * suc k))
      div-div2 zero fi i<j = subst (λ g → Dividable (suc k) g) (begin
          0 ≡⟨ sym (minus<=0 {0} {fi * suc k} z≤n ) ⟩
          0 -  (fi * suc k) ≡⟨ refl ⟩
          (zero * suc k) - (fi * suc k) ∎ ) div0
          where open ≡-Reasoning  
      div-div2 (suc fj) fi i<j with <-cmp fi fj
      ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c i<j  )
      ... | tri≈ ¬a refl ¬c = record { factor = 1 ; is-factor = (begin
             1 * suc k + 0 ≡⟨ +-comm _ 0 ⟩
               1 * suc k ≡⟨ cong suc (+-comm _ 0) ⟩
             suc k ≡⟨ sym (minus+y-y {suc k} {fj * suc k}) ⟩
             (suc k + fj * suc k) - (fj * suc k) ≡⟨ refl ⟩
             (suc (k + fj * suc k)) - (fj * suc k) ∎  )} where open ≡-Reasoning  
      ... | tri< fi<fj ¬b ¬c = record { factor = suc (Dividable.factor (div-div2 fj fi fi<fj )) ; is-factor = ( begin 
          suc (Dividable.factor (div-div2 fj fi fi<fj )) * suc k + 0 ≡⟨ +-comm _ 0 ⟩
          suc (Dividable.factor (div-div2 fj fi fi<fj )) * suc k  ≡⟨ refl ⟩
          suc k + ((Dividable.factor (div-div2 fj fi fi<fj )) * suc k )  ≡⟨ cong (λ g → suc k + g ) (+-comm 0 _) ⟩
          suc k + ((Dividable.factor (div-div2 fj fi fi<fj )) * suc k + 0)  ≡⟨ cong (λ g → suc k + g) (Dividable.is-factor (div-div2 fj fi fi<fj) ) ⟩
          suc k + ((fj * suc k) - (fi * suc k)) ≡⟨ minus+yz {suc k} {fj * suc k} {fi * suc k} (<to≤ (*-monoˡ-< k fi<fj )) ⟩
           ( (suc k + (fj * suc k)) - (fi * suc k)) ≡⟨ refl ⟩
          ((suc fj * suc k) - (fi * suc k)) ∎ ) } where
             open ≡-Reasoning  
   div-div0 : { i j : ℕ } →  Dividable (suc k) i →  Dividable (suc k) j → Dividable (suc k) (i - j) ∧ Dividable (suc k) (j - i)
   div-div0 {i} {j} di dj with <-cmp i j
   ... | tri< a ¬b ¬c    = ⟪ subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {j} (<to≤ a))) div0 , div-div1 di dj a ⟫ 
   ... | tri≈ ¬a refl ¬c = ⟪ subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {i} refl-≤)) div0 ,
                             subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {i} refl-≤)) div0 ⟫
   ... | tri> ¬a ¬b c    = ⟪ div-div1 dj di c , subst (λ g → Dividable (suc k) g) (sym (minus<=0 {j} {i} (<to≤ c))) div0  ⟫ 

open _∧_

gcd-gt : ( i i0 j j0 k : ℕ ) → k > 1 → (if : Factor k i) (i0f : Dividable k i0 ) (jf : Factor k j ) (j0f : Dividable k j0)
   → Dividable k (i - j) ∧ Dividable k (j - i)
   → Dividable k ( gcd1 i i0 j j0 ) 
gcd-gt zero i0 zero j0 k k>1 if i0f jf j0f i-j with <-cmp i0 j0
... | tri< a ¬b ¬c = i0f 
... | tri≈ ¬a refl ¬c = i0f
... | tri> ¬a ¬b c = j0f
gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f i-j = ⊥-elim (div1 k>1 (proj2 i-j)) -- can't happen
gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f i-j = j0f
gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f i-j =   
    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k k>1 (decf (DtoF i0f)) i0f (decf jf) (proj2 i-j) (div-div k>1 i0f (proj2 i-j))
gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f i-j  = ⊥-elim (div1 k>1 (proj1 i-j)) -- can't happen
gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f i-j  = i0f
gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f i-j  = --   
     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) (proj1 i-j) (decf (DtoF j0f)) j0f (div-div k>1 (proj1 i-j) j0f )
gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f i-j  =  
     gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i-j
gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f i-j  = 
     gcd-gt (suc i) i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i-j 

gcd-div : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j ) 
   → Dividable k ( gcd i  j ) 
gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf (div-div k>1 if jf)

gcd-divable : ( i j  : ℕ )
      → Dividable ( gcd i j ) i ∧ Dividable ( gcd i j ) j
gcd-divable i j  = f-induction {_} {_} {ℕ ∧ ℕ}
   {λ p  → Dividable ( gcd (proj1 p) (proj2 p) ) (proj1 p) ∧ Dividable ( gcd (proj1 p)  (proj2 p) ) (proj2 p)} F I ⟪ i , j ⟫ where
        F : ℕ ∧ ℕ → ℕ
        F ⟪ 0 , 0 ⟫ = 0
        F ⟪ 0 , suc j ⟫ = 0
        F ⟪ suc i , 0 ⟫ = 0
        F ⟪ suc i , suc j ⟫ with <-cmp i j
        ... | tri< a ¬b ¬c = suc j
        ... | tri≈ ¬a b ¬c = 0
        ... | tri> ¬a ¬b c = suc i
        F0 : { i j : ℕ } → F ⟪ i , j ⟫ ≡ 0 → (i ≡ j) ∨ (i ≡ 0 ) ∨ (j ≡ 0)
        F0 {zero} {zero} p = case1 refl
        F0 {zero} {suc j} p =  case2 (case1 refl)
        F0 {suc i} {zero} p =  case2 (case2 refl)
        F0 {suc i} {suc j} p with <-cmp i j
        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
        ... | tri≈ ¬a refl ¬c =  case1 refl
        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
        F00 :  {p : ℕ ∧ ℕ} → F p ≡ zero → Dividable (gcd (proj1 p) (proj2 p)) (proj1 p) ∧ Dividable (gcd (proj1 p) (proj2 p)) (proj2 p)
        F00 {⟪ i , j ⟫} eq with F0 {i} {j} eq
        ... | case1 refl = ⟪  subst (λ k → Dividable k i) (sym (gcdmm i i)) div= , subst (λ k → Dividable k i) (sym (gcdmm i i)) div= ⟫
        ... | case2 (case1 refl) = ⟪  subst (λ k → Dividable k i) (sym (trans (gcdsym {0} {j} ) (gcd20 j)))div0
                                    , subst (λ k → Dividable k j) (sym (trans (gcdsym {0} {j}) (gcd20 j))) div= ⟫
        ... | case2 (case2 refl) = ⟪  subst (λ k → Dividable k i) (sym (gcd20 i)) div=
                                    , subst (λ k → Dividable k j) (sym (gcd20 i)) div0 ⟫
        Fsym :  {i j : ℕ } → F ⟪ i , j ⟫ ≡ F ⟪ j , i ⟫
        Fsym {0} {0} = refl
        Fsym {0} {suc j} = refl
        Fsym {suc i} {0} = refl
        Fsym {suc i} {suc j} with <-cmp i j | <-cmp j i
        ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁)
        ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (¬b (sym b))
        ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
        ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl)
        ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
        ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)
        ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
        ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b))
        ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁)
        record Fdec ( i j : ℕ ) : Set where
           field
               ni : ℕ 
               nj : ℕ 
               fdec :  0 < F ⟪ i , j ⟫  → F ⟪ ni , nj ⟫  < F ⟪ i , j ⟫
        fd1 : ( i j k : ℕ ) → i < j  → k ≡ j - i →  F ⟪ suc i , k ⟫ < F ⟪ suc i , suc j ⟫
        fd1 i j 0 i<j eq = ⊥-elim ( nat-≡< eq (minus>0 {i} {j} i<j )) 
        fd1 i j (suc k) i<j eq = fd2 i j k i<j eq where
               fd2 : ( i j k : ℕ ) → i < j → suc k ≡ j - i  →  F ⟪ suc i , suc k ⟫ < F ⟪ suc i , suc j ⟫
               fd2 i j k i<j eq with <-cmp i k | <-cmp i j
               ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = fd3 where
                    fd3 : suc k < suc j  -- suc j - suc i < suc j
                    fd3 = subst (λ g → g < suc j) (sym eq) (y-x<y {suc i} {suc j} (s≤s z≤n) (s≤s z≤n))
               ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (⊥-elim (¬a i<j))
               ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim (⊥-elim (¬a i<j))
               ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = s≤s z≤n
               ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (¬a₁ i<j)
               ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c =  s≤s z≤n -- i > j
               ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = fd4 where
                    fd4 : suc i < suc j
                    fd4 = s≤s a
               ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c =  ⊥-elim (¬a₁ i<j)
               ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ =  ⊥-elim (¬a₁ i<j)
        fedc0 : (i j : ℕ ) → Fdec i j
        fedc0 0 0 = record { ni =  0 ; nj = 0 ; fdec = λ ()  } 
        fedc0 (suc i) 0 = record { ni =  suc i ; nj = 0 ; fdec = λ ()  } 
        fedc0 0 (suc j)  = record { ni =  0 ; nj = suc j ; fdec = λ ()  } 
        fedc0 (suc i) (suc j) with <-cmp i j
        ... | tri< i<j ¬b ¬c = record { ni =  suc i ; nj = j - i ; fdec = λ lt → fd1 i j (j - i) i<j refl  } 
        ... | tri≈ ¬a refl ¬c = record { ni =  suc i ; nj = suc j     ; fdec = λ lt → ⊥-elim (nat-≡< fd0 lt) } where
              fd0 : {i : ℕ } → 0 ≡ F ⟪ suc i , suc i ⟫
              fd0 {i} with <-cmp i i
              ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
              ... | tri≈ ¬a b ¬c = refl
              ... | tri> ¬a ¬b c =  ⊥-elim ( ¬b refl )
        ... | tri> ¬a ¬b c = record { ni =  i - j ; nj = suc j ; fdec = λ lt →
            subst₂ (λ s t → s < t) (Fsym {suc j} {i - j}) (Fsym {suc j} {suc i}) (fd1 j i (i - j) c refl ) } 
        ind :   ( i j : ℕ ) →
            Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.ni (fedc0 i j))
            ∧ Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.nj (fedc0 i j))
             → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
        ind zero zero prev = ind0 where
           ind0 : Dividable (gcd zero zero) zero ∧ Dividable (gcd zero zero) zero
           ind0 = ⟪ div0 , div0 ⟫
        ind zero (suc j) prev = ind1 where
           ind1 : Dividable (gcd zero (suc j)) zero ∧ Dividable (gcd zero (suc j)) (suc j)
           ind1 = ⟪ div0 , subst (λ k → Dividable k (suc j)) (sym (trans (gcdsym {zero} {suc j}) (gcd20 (suc j)))) div=  ⟫
        ind (suc i) zero prev = ind2 where
           ind2 : Dividable (gcd (suc i) zero) (suc i) ∧ Dividable (gcd (suc i) zero) zero
           ind2 = ⟪  subst (λ k → Dividable k (suc i)) (sym (trans refl (gcd20 (suc i)))) div= , div0 ⟫
        ind (suc i) (suc j) prev with <-cmp i j
        ... | tri< a ¬b ¬c = ⟪ ind3 (suc i) (proj1 prev)   , ind4 (proj2 prev) ⟫ where
            ind3 : (s : ℕ ) → Dividable (gcd1 (suc i) (suc i) (j - i) (j - i)) s
                 → Dividable (gcd1 (suc i) (suc i) (suc j) (suc j)) s 
            ind3 s prev = 
               subst (λ k → Dividable k s) ( begin
                 gcd (suc i) (j - i)  ≡⟨ gcdsym {suc i} {j - i} ⟩
                 gcd (j - i ) (suc i)   ≡⟨ sym (gcd+j (j - i) (suc i)) ⟩
                 gcd ((j - i) + suc i) (suc i)  ≡⟨ cong (λ k → gcd k (suc i)) ( begin
                  (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans ( s≤s a) a<sa ) ⟩ -- i ≤ n →  suc (suc i) ≤ suc (suc (suc n)) 
                  suc j ∎ ) ⟩
                 gcd (suc j) (suc i)  ≡⟨ gcdsym {suc j} {suc i} ⟩
                 gcd (suc i) (suc j)  ∎ ) prev where open ≡-Reasoning 
            ind4 : Dividable (gcd (suc i) (j - i)) (j - i) → Dividable (gcd (suc i) (suc j)) (suc j)
            ind4 = {!!}
        ... | tri≈ ¬a b ¬c = {!!}
        ... | tri> ¬a ¬b c = {!!}
        --ind3 where
        --   ind3 : Dividable (gcd (suc i) (suc j)) (suc i) ∧ Dividable (gcd (suc i) (suc j)) (suc j)
        --   ind3 = {!!}

        I : Finduction (ℕ ∧ ℕ) _ F
        I = record {
              fzero = F00 
            ; pnext = λ p → ⟪ Fdec.ni (fedc0 (proj1 p) (proj2 p)) ,  Fdec.nj (fedc0 (proj1 p) (proj2 p)) ⟫ 
            ; decline = λ {p} lt → Fdec.fdec (fedc0 (proj1 p) (proj2 p))  lt
            ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev
          } 


gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1
gcdmul+1 zero n = gcd204 n
gcdmul+1 (suc m) n = begin
      gcd (suc m * n + 1) n ≡⟨⟩
      gcd (n + m * n + 1) n ≡⟨ cong (λ k → gcd k n ) (begin
         n + m * n + 1 ≡⟨ cong (λ k → k + 1) (+-comm n _) ⟩
         m * n + n + 1 ≡⟨ +-assoc (m * n) _ _ ⟩
         m * n + (n + 1)  ≡⟨ cong (λ k → m * n + k) (+-comm n _) ⟩
         m * n + (1 + n)  ≡⟨ sym ( +-assoc (m * n) _ _ ) ⟩
         m * n + 1 + n ∎ 
       ) ⟩
      gcd (m * n + 1 + n) n ≡⟨ gcd+j (m * n + 1) n ⟩
      gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩
      1 ∎ where open ≡-Reasoning

div+1 : { i k : ℕ } → k > 1 →  Dividable k i →  ¬ Dividable k (suc i)  
div+1 {i} {k} k>1 d d1 = div1 k>1 div+11 where
   div+11 : Dividable k 1
   div+11 = subst (λ g → Dividable k g) (minus+y-y {1} {i} ) ( proj2 (div-div k>1 d d1  ) )

gcd>0 : ( i j : ℕ ) → 0 < i → 0 < j → 0 < gcd i j  
gcd>0 i j 0<i 0<j = gcd>01 i i j j 0<i 0<j where
     gcd>01 : ( i i0 j j0 : ℕ ) → 0 < i0 → 0 < j0  → gcd1 i i0 j j0 > 0
     gcd>01 zero i0 zero j0 0<i 0<j with <-cmp i0 j0
     ... | tri< a ¬b ¬c = 0<i
     ... | tri≈ ¬a refl ¬c = 0<i
     ... | tri> ¬a ¬b c = 0<j
     gcd>01 zero i0 (suc zero) j0 0<i 0<j = s≤s z≤n
     gcd>01 zero zero (suc (suc j)) j0 0<i 0<j = 0<j 
     gcd>01 zero (suc i0) (suc (suc j)) j0 0<i 0<j = gcd>01 i0 (suc i0) (suc j) (suc (suc j)) 0<i (s≤s z≤n) -- 0 < suc (suc j)
     gcd>01 (suc zero) i0 zero j0 0<i 0<j =  s≤s z≤n
     gcd>01 (suc (suc i)) i0 zero zero 0<i 0<j = 0<i 
     gcd>01 (suc (suc i)) i0 zero (suc j0) 0<i 0<j = gcd>01 (suc i) (suc (suc i))  j0 (suc j0) (s≤s z≤n) 0<j 
     gcd>01 (suc i) i0 (suc j) j0 0<i 0<j = subst (λ k → 0 < k ) (sym (gcd033 i i0 j j0 )) (gcd>01 i i0 j j0 0<i 0<j ) where
         gcd033 : (i i0 j j0  : ℕ) → gcd1 (suc i) i0 (suc j) j0 ≡  gcd1 i i0 j j0
         gcd033 zero zero zero zero = refl
         gcd033 zero zero (suc j) zero = refl
         gcd033 (suc i) zero j zero = refl
         gcd033 zero zero zero (suc j0) = refl
         gcd033 (suc i) zero zero (suc j0) = refl
         gcd033 zero zero (suc j) (suc j0) = refl
         gcd033 (suc i) zero (suc j) (suc j0) = refl
         gcd033 zero (suc i0) j j0 = refl
         gcd033 (suc i) (suc i0) j j0 = refl