--- a/src/HyperReal.agda	Mon Jul 05 08:55:20 2021 +0900
+++ b/src/HyperReal.agda	Mon Jul 05 09:18:37 2021 +0900
@@ -113,13 +113,23 @@
           suc (suc (i + suc j       + suc (suc (i + suc j + suc (nxn→n i (suc j)))))) ≡⟨ refl ⟩
           nxn→n (suc (suc i)) (suc j) ∎ where
              open ≡-Reasoning
+
+     nn004 : {k k0 : ℕ} → nxn→n 0 k ≡  nxn→n 0 k0 → k ≡ k0
+     nn004 {zero} {zero} eq = refl
+     nn004 {zero} {suc k0} eq = {!!}
+     nn004 {suc k} {zero} eq = {!!}
+     nn004 {suc k} {suc k0} eq = begin
+          suc k ≡⟨ cong suc (nn004 {k} {k0} {!!} ) ⟩ -- k + suc (nxn→n zero k) ≡ k0 + suc (nxn→n zero k0) → nxn→n 0 k ≡ nxn→n 0 k0
+          suc k0 ∎ where
+             open ≡-Reasoning
+
      nn : ( i  : ℕ) → NN i nxn→n n→nxn
      nn zero = record { j = 0 ; k = 0 ; sum = 0 ; stage = 0 ; nn = refl ; ni = refl ; k1 = refl ; k0 = refl
         ;  nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) }
      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 = nn03 ;  nn-unique = {!!} } where
+         ; ni = nn01 ; k1 = nn02 ; k0 = nn03 ;  nn-unique = nn04 } where
             sum = NN.sum (nn i)
             stage = NN.stage (nn i)
             j = NN.j (nn i)