# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1609529360 -32400
# Node ID ba7d4cc92e608dac5b04326549e4ec319a089947
# Parent  d78fc1951c2656fe4ba3642457a8fed19c0e9344
... gcd (i + j) j ≡ gcd i j

diff -r d78fc1951c26 -r ba7d4cc92e60 agda/gcd.agda
--- a/agda/gcd.agda	Sat Jan 02 03:43:24 2021 +0900
+++ b/agda/gcd.agda	Sat Jan 02 04:29:20 2021 +0900
@@ -86,51 +86,6 @@
        comp : ℕ
        is-comp : n * comp ≡ m
 
-gcd27 : (n m i : ℕ) → 1 < m  → gcd n i ≡ m → Comp m n ∨ Comp m i
-gcd27 n m i 1<m gn = gcd271 n n i i gn where
-    gcd271 : (n n0 i i0 : ℕ ) → gcd1 n n0 i i0 ≡ m → Comp m n0 ∨ Comp m i0
-    gcd271 zero n0 zero i0 eq with <-cmp n0 i0
-    ... | tri< a ¬b ¬c = case2 (record { non-1 = 1<m ; comp = 1 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
-    ... | tri≈ ¬a refl ¬c = case1 (record { non-1 = 1<m ; comp = 1 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
-    ... | tri> ¬a ¬b c = case1 (record { non-1 = 1<m ; comp = 1 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
-    gcd271 zero n0 (suc zero) i0 eq = ⊥-elim ( nat-≡< eq 1<m )
-    gcd271 zero zero (suc (suc i)) i0 eq = case2 (record { non-1 = 1<m ; comp = 1 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
-    gcd271 zero (suc n0) (suc (suc i)) i0 eq with gcd271 n0 (suc n0) (suc i) (suc (suc i)) eq
-    ... | case1 t = case1 t
-    -- t : Comp m (suc (suc i)),    (suc n0) + (suc (suc i)) ≡ i0
-    ... | case2 t = case1 (gcd272 t) where
-      gcd272 : Comp m (suc (suc i)) → Comp m (suc n0)
-      gcd272 = {!!}
-    gcd271 (suc zero) n0 zero i0 eq = ⊥-elim ( nat-≡< eq 1<m )
-    gcd271 (suc (suc n)) n0 zero zero eq = case2 (record { non-1 = 1<m ; comp = n0 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
-    gcd271 (suc (suc n)) n0 zero (suc i0) eq = {!!}
-    gcd271 (suc n) n0 (suc i) i0 eq = gcd271 n n0 i i0 (trans (sym (gcd22 n n0 i i0)) eq )
-
-gcd26 : (n m i : ℕ) → 1 < n → 1 < m  → gcd n i ≡ m → ¬ ( gcd n m ≡ 1 )
-gcd26 n m i 1<n 1<m gi g1 = gcd261 n n m m i i 1<n 1<m gi g1 where
-    gcd261 : (n n0 m m0 i i0 : ℕ) → 1 < n → 1 < m0  → gcd1 n n0 i i0 ≡ m0 → ¬ ( gcd1 n n0 m m0 ≡ 1 )
-    gcd261 zero n0 m m0 i i0 () 1<m gi g1
-    -- gi       : gcd1 (suc n) n0 zero i0 ≡ m0
-    -- g1       : gcd1 (suc n) n0 m m0 ≡ 1
-    gcd261 (suc zero) n0 m m0 zero i0 1<n 1<m gi g1 = ⊥-elim (  nat-≡< gi 1<m )
-    gcd261 (suc (suc n)) n0 zero m0 zero zero 1<n 1<m gi g1 = {!!}
-    gcd261 (suc (suc n)) n0 zero m0 zero (suc i0) 1<n 1<m gi g1 = {!!}
-    gcd261 (suc (suc n)) n0 (suc zero) m0 zero i0 1<n 1<m gi g1 = {!!}
-    gcd261 (suc (suc n)) n0 (suc (suc m)) m0 zero zero 1<n 1<m gi g1 = {!!}
-    gcd261 (suc (suc n)) n0 (suc (suc m)) m0 zero (suc i0) 1<n 1<m gi g1 = {!!}
-    -- gi       : gcd1 (suc n) n0 (suc i) i0 ≡ m0
-    -- g1       : gcd1 (suc n) n0 zero m0 ≡ 1
-    gcd261 (suc n) n0 zero m0 (suc i) i0 1<n 1<m gi g1 = {!!}
-    gcd261 (suc zero) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = ⊥-elim ( nat-<≡ 1<n  )
-    gcd261 (suc (suc zero)) n0 (suc m) m0 (suc zero) i0 1<n 1<m gi g1 = ⊥-elim (  nat-≡< gi 1<m )
-    -- gi       : gcd1 0 n0 i i0 ≡ m0
-    gcd261 (suc (suc zero)) n0 (suc zero) m0 (suc (suc i)) i0 1<n 1<m gi refl = {!!}
-    -- gi       : gcd1 0 n0 i i0 ≡ m0
-    -- g1       : gcd1 0 n0 m m0 ≡ 1
-    gcd261 (suc (suc zero)) n0 (suc (suc m)) m0 (suc (suc i)) i0 1<n 1<m gi g1 = {!!}
-    gcd261 (suc (suc (suc n))) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = 
-        gcd261 (suc (suc n)) n0 m m0 i i0 (s≤s (s≤s z≤n)) 1<m gi g1
-
 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₁) 
@@ -175,55 +130,30 @@
           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 : ℕ) → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0
-       -- gcd200 i i0 zero j0 = subst₂ (λ m k → gcd1 m k zero j0 ≡ gcd1 i i0 zero j0 ) (+-comm zero i) (+-comm zero i0) refl
        gcd200 i i0 zero j0 = {!!}
        gcd200 (suc (suc i)) i0 (suc j) (suc j0) = gcd201 (suc (suc i)) i0 j (suc j0) (suc j)
        gcd200 zero zero (suc zero) j0 = {!!}
        gcd200 zero zero (suc (suc j)) j0 = {!!}
        gcd200 zero (suc i0) (suc j) j0 = {!!}
        gcd200 (suc zero) i0 (suc j) j0 = {!!}
-       gcd200 (suc (suc i)) i0 (suc j) zero = ?
+       gcd200 (suc (suc i)) i0 (suc j) zero = {!!}
+
+gcd4 : ( n k : ℕ ) → gcd n k ≡ k → k ≤ n
+gcd4 n k gn = gcd40 n n k k gn where
+       gcd40 :  (i i0 j j0 : ℕ) → gcd1 i i0 j j0 ≡ j0 → j0 ≤ i0
+       gcd40 zero i0 zero j0  gn = {!!}
+       gcd40 zero i0 (suc j) j0 gn = {!!}
+       gcd40 (suc i) i0 zero j0 gn = {!!}
+       gcd40 (suc i) i0 (suc j) j0 gn = gcd40 i i0 j j0 (subst (λ k → k ≡ j0) (gcd22 i i0 j j0) gn)
+
+gcd3 : ( n k : ℕ ) → n ≤ k + k → gcd n k ≡ k → n ≡ k
+gcd3 n k n<2k gn = {!!}
+
+gcd23 : ( n m k : ℕ) → gcd n k ≡ k → gcd m k ≡ k → k ≤ gcd n m 
+gcd23 = {!!}
 
 gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
-gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = gcd21 n n m m k k 1<n 1<m 1<k gn gm gnm where
-   gcd23 : {i0 j0 : ℕ } → 1 < i0  → 1 < j0 → 1 < gcd1 zero i0 zero j0
-   gcd23 {i0} {j0} 1<i 1<j with <-cmp i0 j0
-   ... | tri< a ¬b ¬c = 1<j
-   ... | tri≈ ¬a refl ¬c = 1<i
-   ... | tri> ¬a ¬b c = 1<i
-   1<ss : {j : ℕ} → 1 < suc (suc j)
-   1<ss = s≤s (s≤s z≤n)
-   gcd21 : ( i i0 j j0 o o0 : ℕ ) → 1 < i0 → 1 < j0 → 1 < o0 →  gcd1 i i0 o o0 ≡ k → gcd1 j j0 o o0 ≡ k → gcd1 i i0 j j0 ≡ 1 → ⊥
-   gcd21 zero i0 zero j0 o o0 1<i 1<j 1<o refl gm gnm = nat-≡< (sym gnm) (gcd23 1<i 1<j)
-   gcd21 zero i0 (suc j) j0 zero o0 1<i 1<j 1<o refl gm gnm = gcd25 i0 o0 j j0 1<o 1<i 1<k gm (subst (λ k → k ≡ 1) (gcdsym1 zero _ (suc j) _) gnm)  where
-      -- gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ suc (suc i0) , gcd1 (suc j) (suc (suc j)) (suc i0) (suc (suc i0)) ≡ 1
-      gcd25 : (i0 o0 j j0 : ℕ) → 1 < o0 → 1 < i0
-            → 1 < gcd1 zero i0 zero o0 
-            → ( gm : gcd1 (suc j) j0 zero o0 ≡ gcd1 zero i0 zero o0 ) → (gnm : gcd1 (suc j) j0 zero i0 ≡ 1) → ⊥
-      gcd25 i0 o0 zero j0 1<o 1<i 1<k gm refl with <-cmp i0 o0
-      ... | tri< a ¬b ¬c    = ⊥-elim ( nat-≡< gm 1<o )
-      ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< gm 1<o )
-      ... | tri> ¬a ¬b c    = ⊥-elim ( nat-≡< gm 1<i )
-      -- gm       : gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ (gcd1 zero (suc i0) zero (suc (suc o0))
-      --            gcd1 j       (suc (suc j))       o0 (suc (suc o0)) 
-      -- gnm      : gcd1 (suc j) (suc (suc j)) i0 (suc i0) ≡ 1
-      gcd25 i0       (suc zero)     (suc j) j0 1<o 1<i 1<k gm gnm = {!!} -- ⊥-elim ( nat-≤> (subst (λ k → k ≤ 1 ) gm (gcd27 (suc j) (suc (suc j)))) 1<k )
-      gcd25 (suc zero) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm = {!!}
-      --     (suc (suc i0)) > (suc (suc o0)) → gm = gnm → (suc (suc i0)) ≡ 1
-      --     (suc (suc i0)) < (suc (suc o0)) → ? gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡  (suc (suc o0)) 
-      --                                         gcd1 (suc j) (suc (suc j)) (suc i0) (suc (suc i0)) ≡  1
-      gcd25 (suc (suc i0)) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm with <-cmp  (suc (suc i0))   (suc (suc o0))
-      ... | tri< a ¬b ¬c = {!!}
-      ... | tri≈ ¬a b ¬c = {!!}
-      ... | tri> ¬a ¬b c = gcd26 {!!} {!!} {!!} {!!} {!!} {!!} {!!}
-   gcd21 zero i0 (suc j) j0 (suc zero) o0 1<i 1<j 1<o refl gm gnm = nat-<≡ 1<k
-   gcd21 zero (suc i0) (suc j) j0 (suc (suc o)) o0 1<i 1<j 1<o gn gm gnm = 
-       gcd21 i0 {!!} (suc j) j0 (suc o) (suc (suc o)) 1<i 1<j {!!} gn {!!} {!!}
-   gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn gm gnm = {!!}
-   gcd21 (suc i) i0 (suc j) j0 zero o0 1<i 1<j 1<o gn gm gnm = {!!}
-   gcd21 (suc i) i0 (suc j) j0 (suc o) o0 1<i 1<j 1<o gn gm gnm = 
-       gcd21 i i0 j j0 o o0 1<i 1<j 1<o (subst (λ m → m ≡ k) (gcd22 i i0 _ _ ) gn)
-                                        (subst (λ m → m ≡ k) (gcd22 j j0 _ _ ) gm) (subst (λ k → k ≡ 1) (gcd22 i i0 _ _ ) gnm)
+gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = ⊥-elim ( nat-≡< (sym gnm) (≤-trans 1<k (gcd23 n m k gn gm  )))
 
 record Even (i : ℕ) : Set where
   field