# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585546094 -32400
# Node ID 73511e7ddf5cea09c054053fc6d096dc632ac723
# Parent  fd8633b6d551395078809f4d9b5162e90bfb4317
u2 done

diff -r fd8633b6d551 -r 73511e7ddf5c prob1.agda
--- a/prob1.agda	Mon Mar 30 10:31:16 2020 +0900
+++ b/prob1.agda	Mon Mar 30 14:28:14 2020 +0900
@@ -38,7 +38,7 @@
    field
       c1 : Cond1 A M k
       u1 : {j m : ℕ} → j < Cond1.i c1  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
-      -- u2 : {j m : ℕ} → Cond1.i c1  < j → j < M  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
+      u2 : {j m : ℕ} → Cond1.i c1  < j → j < M  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
       -- u3 : {j m : ℕ} → j < M → m < Cond1.n c1  → ¬ ( j + k * M  ≡ M * (suc m) + A    )
       -- u4 : {j m : ℕ} → j < M → Cond1.n c1 < m  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
 
@@ -70,10 +70,10 @@
         lemma4 : {i j x y z : ℕ} → j + x ≡ y → i + x ≡ z → j < i → y < z
         lemma4 {i} {j} {x} refl refl (s≤s z≤n) = s≤s (subst (λ k → x ≤ k ) (+-comm x _) x≤x+y)
         lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) )
-        lemma5 : {m1  : ℕ} →      M * suc m1 + A  < M * suc n + A
+        lemma5 : {m1 n : ℕ} →      M * suc m1 + A  < M * suc n + A
                            → M + (M * suc m1 + A) ≤ M * suc n + A  
-        lemma5 {m1} lt with <-cmp m1 n
-        lemma5 {m1} lt | tri< a ¬b ¬c = begin
+        lemma5 {m1} {n} lt with <-cmp m1 n
+        lemma5 {m1} {n} lt | tri< a ¬b ¬c = begin
                    M + (M * suc m1 + A)
                ≡⟨ sym (+-assoc M _ _ ) ⟩
                    (M + M * suc m1) + A
@@ -84,8 +84,8 @@
                ≤⟨ ≤-plus {_} {_} {A} (subst₂ (λ x y → x ≤ y ) (*-comm _ M ) (*-comm _ M )  (*≤ (s≤s a))) ⟩
                    M * suc n + A
                ∎ where open ≤-Reasoning
-        lemma5 {m1} lt | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<≡ lt )
-        lemma5 {m1} lt | tri> ¬a ¬b c = ⊥-elim ( nat-<> lt (<-plus {_} {_} {A} (<≤+ (s≤s c)
+        lemma5 {m1} {n} lt | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<≡ lt )
+        lemma5 {m1} {n} lt | tri> ¬a ¬b c = ⊥-elim ( nat-<> lt (<-plus {_} {_} {A} (<≤+ (s≤s c)
                 (subst₂ (λ x y → x ≤ y ) (*-comm _ m ) (*-comm _ m ) (*≤ (s≤s (≤to< c)))))))
         lemma6 : {i j x : ℕ} → M + (j + x ) ≤ i + x → M ≤ i
         lemma6 {i} {j} {x} lt = ≤-minus {M} {i} {x} (x+y≤z→x≤z ( begin 
@@ -97,15 +97,25 @@
                ≤⟨ lt  ⟩
                  i + x 
                ∎ )) where open ≤-Reasoning
-        lemma-u1 : {j : ℕ} {m1 : ℕ} → j < (A - ((k - n) * M)) → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A
+        i : ℕ
+        i = A - ((k - n) * M)
+        lemma-u1 : {j : ℕ} {m1 : ℕ} → j < i → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A
         lemma-u1 {j} {m1} j<akM m1<k eq with <-cmp j M
         lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c =
             ⊥-elim (nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym eq) (sym (Cond1.rule1 c1 )) (lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM ))) ) i<M ) where
-             lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A
+             lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A   -- M + j ≤ i
              lemma3 = lemma5 (lemma4  eq (Cond1.rule1 c1) j<akM)
         lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) 
         lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM ) 
-        c0  =  record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = i<M; rule1 = Cond1.rule1 c1 } ; u1 = lemma-u1 }
+        lemma-u2 : {j : ℕ} {m1  : ℕ} → (A - ((k - n) * M)) < j →
+            j < M → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A
+        lemma-u2 {j} {m1} i<j j<M m1<k eq = ⊥-elim ( nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym (Cond1.rule1 c1)) (sym eq) lemma3-2)) j<M ) where
+             lemma3-2 : M + (M * suc n + A) ≤ M * suc m1 + A -- M + i ≤ j
+             lemma3-2 = lemma5 (lemma4 (Cond1.rule1 c1) eq i<j)
+        c0  =  record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = i<M; rule1 = Cond1.rule1 c1 }
+            ; u1 = lemma-u1 
+            ; u2 = lemma-u2
+            }
      --  loop on  range  of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M
      nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M) 
      nextc n n<k with k - n | inspect (_-_ k) n