--- a/src/HyperReal.agda	Sun Jul 04 23:46:55 2021 +0900
+++ b/src/HyperReal.agda	Mon Jul 05 00:46:17 2021 +0900
@@ -82,7 +82,7 @@
      nn (suc i) with NN.k (nn i)  | inspect  NN.k (nn i) 
      ... | zero | record { eq = eq } = record { k = suc (NN.sum (nn i)) ; j = 0 ; sum = suc  (NN.sum (nn i)) ; stage = suc  (NN.sum (nn i)) + (NN.stage (nn i))
          ; nn = refl
-         ; ni = nn01 ; k1 = nn02 ; k0 = {!!} ;  nn-unique = {!!} } where
+         ; ni = nn01 ; k1 = nn02 ; k0 = nn03 ;  nn-unique = {!!} } where
             sum = NN.sum (nn i)
             stage = NN.stage (nn i)
             j = NN.j (nn i)
@@ -98,9 +98,27 @@
                sum + suc (nxn→n 0 sum) ≡⟨ sym (+-assoc sum 1 (nxn→n 0 sum)) ⟩
                (sum + 1) + nxn→n 0 sum  ≡⟨ cong (λ k → k + nxn→n 0 sum )  (+-comm sum 1 )⟩
                suc (sum + nxn→n 0 sum) ≡⟨ cong suc (nid20 sum ) ⟩
-               suc (nxn→n sum 0) ≡⟨ {!!} ⟩
+               suc (nxn→n sum 0) ≡⟨ cong (λ k → suc (nxn→n k 0 )) (sym (NN.nn (nn i))) ⟩
+               suc (nxn→n (NN.j (nn i) + (NN.k (nn i))  ) 0) ≡⟨ cong₂ (λ j k → suc (nxn→n (NN.j (nn i) + j) k )) eq (sym eq)  ⟩
+               suc (nxn→n (NN.j (nn i) + 0 ) (NN.k (nn i))) ≡⟨ cong (λ k → suc ( nxn→n k (NN.k (nn i)))) (+-comm (NN.j (nn i)) 0) ⟩
                suc (nxn→n (NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i) ) ⟩
                suc i ∎  where open ≡-Reasoning
+            nn03 :  n→nxn (suc i) ≡ ⟪ 0 , suc (NN.sum (nn i)) ⟫   -- k0 : n→nxn i ≡ ⟪ NN.j (nn i) = sum , NN.k (nn i) = 0 ⟫
+            nn03 with n→nxn i | inspect  n→nxn i
+            ... | ⟪ x , zero  ⟫ | record { eq = eq1 } = begin
+                ⟪ zero , suc x ⟫ ≡⟨ cong (λ k →  ⟪ zero , suc k ⟫) (sym (cong proj1 eq1)) ⟩
+                ⟪ zero , suc (proj1 (n→nxn i)) ⟫ ≡⟨ cong (λ k →  ⟪ zero , suc k ⟫) (cong proj1 (NN.k0 (nn i)))  ⟩
+                ⟪ zero , suc (NN.j (nn i)) ⟫ ≡⟨  cong (λ k →  ⟪ zero , suc k ⟫) (+-comm 0 _ ) ⟩
+                ⟪ zero , suc (NN.j (nn i) + 0) ⟫ ≡⟨  cong (λ k →  ⟪ zero , suc (NN.j (nn i) + k)  ⟫ ) (sym eq)  ⟩
+                ⟪ zero , suc (NN.j (nn i) + NN.k (nn i)) ⟫ ≡⟨ cong (λ k →  ⟪ zero , suc k ⟫ ) (NN.nn (nn i))  ⟩
+                ⟪ 0 , suc sum  ⟫  ∎  where open ≡-Reasoning
+            ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 (NN.k0 (nn i)))) (begin
+               suc (NN.k (nn i)) ≡⟨ cong suc eq ⟩
+               suc 0 ≤⟨ s≤s z≤n  ⟩
+               suc y ≡⟨ sym (cong proj2 eq1) ⟩
+               proj2 (n→nxn i)  ∎ ))  where open ≤-Reasoning
+            nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (NN.sum (nn i)) ⟫ ≡ ⟪ j0 , k0 ⟫
+            nn04 = ?
      ... | suc k  | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; sum = NN.sum (nn i) ; stage = NN.stage (nn i) ; nn = {!!} ; ni = {!!}
          ; k1 = {!!} ; k0 = {!!} ;  nn-unique = {!!} }