--- a/agda/gcd.agda	Sat Jan 02 18:23:54 2021 +0900
+++ b/agda/gcd.agda	Mon Jan 04 09:24:11 2021 +0900
@@ -11,28 +11,6 @@
 open import nat
 open import logic
 
-even : (n : ℕ ) → Set
-even zero = ⊤
-even (suc zero) = ⊥
-even (suc (suc n)) = even n
-
-even? : (n : ℕ ) → Dec ( even n )
-even? zero = yes tt
-even? (suc zero) = no (λ ())
-even? (suc (suc n)) = even? n
-
-n+even : {n m : ℕ } → even n → even m  → even ( n + m )
-n+even {zero} {zero} tt tt = tt
-n+even {zero} {suc m} tt em = em
-n+even {suc (suc n)} {m} en em = n+even {n} {m} en em
-
-n*even : {m n : ℕ } → even n → even ( m * n )
-n*even {zero} {n} en = tt
-n*even {suc m} {n} en = n+even {n} {m * n} en (n*even {m} {n} en) 
-
-even*n : {n m : ℕ } → even n → even ( n * m )
-even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)
-
 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
 gcd1 zero i0 zero j0 with <-cmp i0 j0
 ... | tri< a ¬b ¬c = i0
@@ -49,13 +27,6 @@
 gcd : ( i j : ℕ ) → ℕ
 gcd i j = gcd1 i i j j 
 
-even→gcd=2 : {n : ℕ} → even n → n > 0 → gcd n 2 ≡ 2
-even→gcd=2 {suc (suc zero)} en (s≤s z≤n) = refl
-even→gcd=2 {suc (suc (suc (suc n)))} en (s≤s z≤n) = begin
-       gcd (suc (suc (suc (suc n)))) 2 ≡⟨⟩
-       gcd (suc (suc n)) 2 ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
-       2 ∎ where open ≡-Reasoning
-
 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
 
@@ -80,12 +51,6 @@
 ... | tri> ¬a ¬b c = refl
 gcdmm (suc n) m  = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m )
 
-record Comp ( m n : ℕ ) : Set where
-   field
-       non-1 : 1 < m
-       comp : ℕ
-       is-comp : n * comp ≡ 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₁) 
@@ -156,102 +121,86 @@
           gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning
        gcd200 (suc (suc i)) i0 (suc j) zero i=i0 ()
 
+gcd52 : {i : ℕ } → 1 < suc (suc i)
+gcd52 {zero} = a<sa
+gcd52 {suc i} = <-trans (gcd52 {i}) a<sa
+
+gcd50 : (i i0 j j0 : ℕ) → 1 < i0 → i ≤ i0 → j ≤ j0 →  gcd1 i i0 j j0 ≤ i0 
+gcd50 zero i0 zero j0 0<i i<i0 j<j0 with <-cmp i0 j0
+... | tri< a ¬b ¬c = ≤-refl    
+... | tri≈ ¬a refl ¬c =  ≤-refl 
+... | tri> ¬a ¬b c = ≤-trans refl-≤s c  
+gcd50 zero (suc i0) (suc zero) j0 0<i i<i0 j<j0 = gcd51 0<i where 
+   gcd51 : 1 < suc i0 → gcd1 zero (suc i0) 1 j0 ≤ suc i0
+   gcd51 1<i = ≤to< 1<i
+gcd50 zero (suc i0) (suc (suc j)) j0 0<i i<i0 j<j0 = gcd50 i0 (suc i0) (suc j) (suc (suc j)) 0<i refl-≤s refl-≤s
+gcd50 (suc zero) i0 zero j0 0<i i<i0 j<j0 = ≤to< 0<i
+gcd50 (suc (suc i)) i0 zero zero 0<i i<i0 j<j0 = ≤-refl
+gcd50 (suc (suc i)) i0 zero (suc j0) 0<i i<i0 j<j0 = ≤-trans (gcd50 (suc i) (suc (suc i))  j0 (suc j0) gcd52  refl-≤s refl-≤s) i<i0
+gcd50 (suc i) i0 (suc j) j0 0<i i<i0 j<j0 = subst (λ k → k ≤ i0 ) (sym (gcd22 i i0 j j0))
+   (gcd50 i i0 j j0 0<i (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0)) 
+
 gcd5 : ( n k : ℕ ) → 1 < n → gcd n k ≤ n
-gcd5 n k 0<n = gcd50 n n k k 0<n ≤-refl ≤-refl where
-    gcd52 : {i : ℕ } → 1 < suc (suc i)
-    gcd52 {zero} = a<sa
-    gcd52 {suc i} = <-trans (gcd52 {i}) a<sa
-    gcd50 : (i i0 j j0 : ℕ) → 1 < i0 → i ≤ i0 → j ≤ j0 →  gcd1 i i0 j j0 ≤ i0 
-    gcd50 zero i0 zero j0 0<i i<i0 j<j0 with <-cmp i0 j0
-    ... | tri< a ¬b ¬c = ≤-refl    
-    ... | tri≈ ¬a refl ¬c =  ≤-refl 
-    ... | tri> ¬a ¬b c = ≤-trans refl-≤s c  
-    gcd50 zero (suc i0) (suc zero) j0 0<i i<i0 j<j0 = gcd51 0<i where 
-       gcd51 : 1 < suc i0 → gcd1 zero (suc i0) 1 j0 ≤ suc i0
-       gcd51 1<i = ≤to< 1<i
-    gcd50 zero (suc i0) (suc (suc j)) j0 0<i i<i0 j<j0 = gcd50 i0 (suc i0) (suc j) (suc (suc j)) 0<i refl-≤s refl-≤s
-    gcd50 (suc zero) i0 zero j0 0<i i<i0 j<j0 = ≤to< 0<i
-    gcd50 (suc (suc i)) i0 zero zero 0<i i<i0 j<j0 = ≤-refl
-    gcd50 (suc (suc i)) i0 zero (suc j0) 0<i i<i0 j<j0 = ≤-trans (gcd50 (suc i) (suc (suc i))  j0 (suc j0) gcd52  refl-≤s refl-≤s) i<i0
-    gcd50 (suc i) i0 (suc j) j0 0<i i<i0 j<j0 = subst (λ k → k ≤ i0 ) (sym (gcd22 i i0 j j0))
-        (gcd50 i i0 j j0 0<i (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0)) 
+gcd5 n k 0<n = gcd50 n n k k 0<n ≤-refl ≤-refl 
+
+gcd6 : ( n k : ℕ ) → 1 < n → gcd k n ≤ n
+gcd6 n k 1<n = subst (λ m → m ≤ n) (gcdsym {n} {k}) (gcd5 n k 1<n)
 
 gcd4 : ( n k : ℕ ) → 1 < n  → gcd n k ≡ k → k ≤ n
 gcd4 n k 1<n eq = subst (λ m → m ≤ n ) eq (gcd5 n k 1<n)
 
-gcd3 : ( n k : ℕ ) → 1 < n → n ≤ k + k → gcd n k ≡ k → n ≡ k
-gcd3 n k 1<n n<2k gn with gcd4 n k 1<n gn | <-cmp n k
-... | k≤n | tri< a ¬b ¬c = ⊥-elim (nat-≤> k≤n a)
-... | k≤n | tri≈ ¬a b ¬c = b
-... | k≤n | tri> ¬a ¬b c = ⊥-elim (nat-≤> k≤n  {!!} )
+record Comp ( m n : ℕ ) : Set where
+   field
+       comp : ℕ
+       is-comp : n * comp ≡ m
+
+open Comp
+
+comp-n : ( m n : ℕ ) → Comp m n → Comp (m + n) n
+comp-n m n c = record { comp = suc (comp c) ; is-comp = 
+   begin
+      n * suc (comp c)  ≡⟨ *-comm n (suc (comp c)) ⟩
+      n + comp c * n ≡⟨ +-comm n (comp c * n) ⟩
+      comp c * n + n ≡⟨ cong (λ k → k + n) ( *-comm (comp c) n) ⟩
+      (n * comp c) + n ≡⟨ cong (λ k → k + n) (is-comp c) ⟩ 
+      m + n ∎ 
+    } where open ≡-Reasoning
+
+gcdcomp : ( m n o : ℕ ) → 0 < n → Set
+gcdcomp m n o 0<n = gcd n m ≡ o → Comp n o 
+
+gcdcomp-eq : ( m o : ℕ ) (0<m : 0 < m)  → gcdcomp m m o 0<m
+gcdcomp-eq m o 0<m g = record { comp = 1 ; is-comp = gcdc0 g } where
+   gcdc0 : (g : gcd m m ≡ o) → o * 1 ≡ m
+   gcdc0 g = begin
+      o * 1 ≡⟨ cong (λ k → k * 1) (sym g) ⟩
+      gcd m m  * 1 ≡⟨ *-identityʳ _ ⟩
+      gcd m m  ≡⟨ gcdmm m m ⟩
+      m ∎ where open ≡-Reasoning
+
+gcd3 : Set
+gcd3 = ( n k : ℕ ) → 1 < n → n < k + k → gcd n k ≡ k → n ≡ k 
+
+0<gcd : {i j : ℕ} → 0 < j → 0 < gcd j i
+0<gcd {zero} {zero} ()
+0<gcd {zero} {suc j} 0<j = subst (λ k → 0 < k ) (sym (gcd20 (suc j))) 0<j
+0<gcd {suc i} {suc j} (s≤s 0<j) = {!!}
 
 gcd23 : ( n m k : ℕ) → 1 < n → 1 < m  → gcd n k ≡ k → gcd m k ≡ k → k ≤ gcd n m 
-gcd23 = {!!}
+gcd23 n m k 1<n 1<m gn gm = gcd230 n n m m k k 1<n 1<m ≤-refl ≤-refl ≤-refl gn gm where
+     gcd231 : (i0 k k0 : ℕ) → (1 < i0) → (suc k ≤ k0) → gcd1 0 i0 (suc k) k0 ≡ suc k → suc k ≤ i0
+     gcd231 i0 k k0 1<i0 sk<k0 gi = subst (λ m → m ≤ i0 ) gi ( gcd50 0 i0 (suc k) k0 1<i0 z≤n sk<k0 )
+     gcd230 : (i i0 j j0 k k0 : ℕ) → 1 < i0 → 1 < j0 → i ≤ i0 → j ≤ j0 → k ≤ k0  → gcd1 i i0 k k0 ≡ k → gcd1 j j0 k k0 ≡ k → k ≤ gcd1 i i0 j j0
+     gcd230 j i0 i j0 zero k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
+     gcd230 zero i0 zero j0 (suc k) k0 1<i 1<j i<i0 j<j0 k<k0 gi gj with <-cmp i0 j0
+     ... | tri< a ¬b ¬c = gcd231 i0 k k0 1<i k<k0 gi   -- k ≤ gcd1 zero i0 (suc j) j0
+     ... | tri≈ ¬a refl ¬c = gcd231 j0 k k0 1<i k<k0 gj 
+     ... | tri> ¬a ¬b c = gcd231 j0 k k0 1<j k<k0 gj 
+     gcd230 zero i0 (suc j) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
+     gcd230 (suc i) i0 zero j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
+     gcd230 (suc i) i0 (suc j) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = subst (λ m → suc k ≤ m) (sym (gcd22 i i0 j j0))
+         (gcd230 i i0 j j0 (suc k) k0 {!!} {!!} {!!} {!!} k<k0 {!!} {!!} ) -- gcd1 (suc i) i0 (suc k) k0 ≡ suc k → gcd1 i i0 (suc k) k0 ≡ suc k
 
 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 = ⊥-elim ( nat-≡< (sym gnm) (≤-trans 1<k (gcd23 n m k 1<n 1<m gn gm  )))
 
-record Even (i : ℕ) : Set where
-  field
-     j : ℕ
-     is-twice : i ≡ 2 * j
-
-e2 : (i : ℕ) → even i → Even i
-e2 zero en = record { j = 0 ; is-twice = refl }
-e2 (suc (suc i)) en = record { j = suc (Even.j (e2 i en )) ; is-twice = e21 } where
-   e21 : suc (suc i) ≡ 2 * suc (Even.j (e2 i en))
-   e21 = begin
-    suc (suc i)  ≡⟨ cong (λ k → suc (suc k)) (Even.is-twice (e2 i en))  ⟩
-    suc (suc (2 * Even.j (e2 i en)))  ≡⟨ sym (*-distribˡ-+ 2 1 _) ⟩
-    2 * suc (Even.j (e2 i en))      ∎ where open ≡-Reasoning
-
-record Odd (i : ℕ) : Set where
-  field
-     j : ℕ
-     is-twice : i ≡ suc (2 * j )
-
-odd2 : (i : ℕ) → ¬ even i → even (suc i) 
-odd2 zero ne = ⊥-elim ( ne tt )
-odd2 (suc zero) ne = tt
-odd2 (suc (suc i)) ne = odd2 i ne 
-
-odd3 : (i : ℕ) → ¬ even i →  Odd i
-odd3 zero ne = ⊥-elim ( ne tt )
-odd3 (suc zero) ne = record { j = 0 ; is-twice = refl }
-odd3 (suc (suc i))  ne = record { j = Even.j (e2 (suc i) (odd2 i ne)) ; is-twice = odd31 } where
-  odd31 : suc (suc i) ≡ suc (2 * Even.j (e2 (suc i) (odd2 i ne)))
-  odd31 = begin
-    suc (suc i) ≡⟨  cong suc (Even.is-twice (e2 (suc i) (odd2 i ne)))  ⟩
-    suc (2 * (Even.j (e2 (suc i) (odd2 i ne))))      ∎ where open ≡-Reasoning
-
-odd4 : (i : ℕ) → even i → ¬ even ( suc i )
-odd4 (suc (suc i)) en en1 = odd4 i en en1 
-
-even^2 : {n : ℕ} → even ( n * n ) → even n
-even^2 {n} en with even? n
-... | yes y = y
-... | no ne = ⊥-elim ( odd4 ((2 * m) + 2 * m * suc (2 * m)) (n+even {2 * m} {2 * m * suc (2 * m)} ee3 ee4) (subst (λ k → even k) ee2 en )) where
-    m : ℕ
-    m = Odd.j ( odd3 n ne )
-    ee3 : even (2 * m)
-    ee3 = subst (λ k → even k ) (*-comm m 2) (n*even {m} {2} tt )
-    ee4 : even ((2 * m) * suc (2 * m))
-    ee4 = even*n {(2 * m)} {suc (2 * m)} (even*n {2} {m} tt )
-    ee2 : n * n ≡ suc (2 * m) + ((2 * m) * (suc (2 * m) ))
-    ee2 = begin n * n ≡⟨ cong ( λ k → k * k) (Odd.is-twice (odd3 n ne)) ⟩
-       suc (2 * m) * suc (2 * m) ≡⟨ *-distribʳ-+ (suc (2 * m)) 1 ((2 * m) ) ⟩
-        (1 * suc (2 * m)) + 2 * m * suc (2 * m) ≡⟨ cong (λ k → k + 2 * m * suc (2 * m)) (begin
-        suc m + 1 * m + 0 * (suc m + 1 * m ) ≡⟨ +-comm (suc m + 1 * m) 0 ⟩
-        suc m + 1 * m  ≡⟨⟩
-        suc (2 * m)  
-        ∎) ⟩ suc (2 * m)  + 2 * m * suc (2 * m) ∎ where open ≡-Reasoning
-
-open import nat
-
-e3 : {i j : ℕ } → 2 * i ≡ 2 * j →  i ≡ j
-e3 {zero} {zero} refl = refl
-e3 {suc x} {suc y} eq with <-cmp x y
-... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (s≤s (<-trans (<-plus a) (<-plus-0 (s≤s (<-plus a ))))))
-... | tri≈ ¬a b ¬c = cong suc b
-... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c ))))))
-