--- a/prob1.agda	Tue Mar 31 01:18:56 2020 +0900
+++ b/prob1.agda	Tue Mar 31 01:43:50 2020 +0900
@@ -66,6 +66,9 @@
      cck-u n n<k k<A i<M = c0 where
         c1 : Cond1 A M (suc k) 
         c1 = cck n n<k k<A i<M 
+
+        --- Uniqueness of i and n
+
         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) )
@@ -135,6 +138,9 @@
         unique-m {i} {_} {n} {m1} refl eqn eqm | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (trans (sym eqm) eqn ) (lemma7 {m1} {n} {m} {A} c ))
         unique-n :  {j m1 : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → n ≡ m1
         unique-n {j} {m1} j<M m1<k eq = unique-m (unique-i j<M m1<k eq ) (Cond1.rule1 c1) eq 
+
+        --- range of A
+
         lemmab : {x m : ℕ } → x <  suc (m + x)
         lemmab {x} {zero} =  a<sa
         lemmab {zero} {suc m} =  <to<s (lemmab {zero} {m})
@@ -191,11 +197,14 @@
                ≤⟨ minus+< {suc k * M} {1} {n * M} ⟩ 
                   (suc k * M ) - 1
                ∎ where open ≤-Reasoning
+
+        c0  : UCond1 A M (suc k)
         c0  =  record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = i<M; rule1 = Cond1.rule1 c1 }
             ; unique-i = unique-i 
             ; unique-n = unique-n
             ; maxA = maxA i<M
             }
+
      --  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