# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1625290021 -32400
# Node ID a9fc3ece852a54cadbd3bc6e77fed8b4badf5cd5
# Parent  b7c2a67befdf021fdb3fd4ee871d655fbd2ce121
...

diff -r b7c2a67befdf -r a9fc3ece852a src/HyperReal.agda
--- a/src/HyperReal.agda	Sat Jul 03 10:46:55 2021 +0900
+++ b/src/HyperReal.agda	Sat Jul 03 14:27:01 2021 +0900
@@ -50,24 +50,70 @@
      ... | ⟪ x , zero ⟫ = ⟪ zero  , suc x ⟫
      ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫
      nid1 : (i : ℕ) → 0 < proj2 ( n→nxn i)  → n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫
-     nid1 (suc i) 0<p2 with  n→nxn (suc i) | inspect  n→nxn (suc i)
-     ... | ⟪ x , zero ⟫ | record { eq = eq } = {!!}
-     ... | ⟪ x , suc y ⟫ | record { eq = eq } = refl
+     nid1 (suc i) 0<p2 with  n→nxn (suc i) 
+     ... | ⟪ x , zero ⟫ = ⊥-elim ( nat-≤> 0<p2 a<sa )
+     ... | ⟪ x , suc y ⟫ = refl
+     nid4 : {i j : ℕ} →  i + 1 + j ≡ i + suc j
+     nid4 {zero} {j} = refl
+     nid4 {suc i} {j} = cong suc (nid4 {i} {j} )
+     nid5 : {i j k : ℕ} →  i + suc (suc j) + suc k ≡ i + suc j + suc (suc k )
+     nid5 {zero} {j} {k} = begin
+          suc (suc j) + suc k ≡⟨ +-assoc 1 (suc j) _ ⟩
+          1 + (suc j + suc k) ≡⟨ +-comm 1 _ ⟩
+          (suc j + suc k) + 1 ≡⟨ +-assoc (suc j) (suc k) _ ⟩
+          suc j + (suc k + 1) ≡⟨ cong (λ k → suc j + k ) (+-comm (suc k) 1) ⟩
+          suc j + suc (suc k) ∎ where open ≡-Reasoning
+     nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} )
      nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
      nid2 zero zero = refl
      nid2 zero (suc j) = refl
-     nid2 (suc i) zero = {!!}
-     nid2 (suc i) (suc j) = {!!}
+     nid2 (suc i) zero = begin
+          suc (nxn→n (suc i) 1)  ≡⟨ refl ⟩
+          suc (suc (i + 1 + suc (nxn→n i 1)))  ≡⟨ cong (λ k → suc (suc k)) nid4  ⟩
+          suc (suc (i + suc (suc (nxn→n i 1))))  ≡⟨ cong (λ k →  suc (suc (i + suc (suc k)))) (nid3 i) ⟩
+          suc (suc (i + suc (suc (i + suc (nxn→n i 0)))))  ≡⟨ refl ⟩
+          nxn→n (suc (suc i)) zero ∎ where
+             open ≡-Reasoning
+             nid3 : (i : ℕ) → nxn→n i 1 ≡ i + suc (nxn→n i 0)
+             nid3 zero = refl
+             nid3 (suc i) = begin
+                 suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩
+                 suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k →  suc (i + suc (suc k))) (nid3 i) ⟩
+                 suc (i + suc (suc (i + suc (nxn→n i 0))))
+              ∎
+     nid2 (suc i) (suc j) = begin
+          suc (nxn→n (suc i) (suc (suc j)))  ≡⟨ refl ⟩
+          suc (suc (i + suc (suc j) + suc (nxn→n i (suc (suc j)))))  ≡⟨ cong (λ k → suc (suc (i + suc (suc j) + k))) (nid2 i (suc j)) ⟩
+          suc (suc (i + suc (suc j) + suc      (i + suc j + suc (nxn→n i (suc j)))))  ≡⟨ cong ( λ k → suc (suc k)) nid5 ⟩
+          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
+     nid6 : {i : ℕ } → 0 < i  → suc (pred i) ≡ i
+     nid6 {suc i} 0<i = refl
      n-id :  (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i
      n-id 0 = refl
-     n-id (suc i) with proj2 (n→nxn (suc i)) 
-     ... | zero = {!!}
-     ... | suc x = begin
-          nxn→n (proj1 (n→nxn (suc i))) (suc x)   ≡⟨ {!!} ⟩
-          nxn→n (proj1 (n→nxn i)) (suc x)   ≡⟨ {!!} ⟩
-          nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))   ≡⟨ {!!} ⟩
-          i   ≡⟨ {!!} ⟩
-          suc i ∎ where open ≡-Reasoning
+     n-id (suc i) with proj2 (n→nxn (suc i))  | inspect  proj2 (n→nxn (suc i))
+     ... | zero  | record { eq = eq } = {!!}
+     ... | suc x | record { eq = eq } with  proj2 (n→nxn i) | inspect proj2 (n→nxn i) 
+     ... | zero  | record { eq = eqy } = {!!}
+     ... | suc y | record { eq = eqy } = begin
+          nxn→n (proj1 (n→nxn (suc i))) (suc x)   ≡⟨ cong (λ k → nxn→n (proj1 k) (suc x)) (nid1 i nid7 ) ⟩
+          nxn→n (suc (proj1 (n→nxn i))) (suc x)   ≡⟨ sym (nid2 (proj1 (n→nxn i)) (suc x) ) ⟩
+          suc (nxn→n (proj1 (n→nxn i)) (suc (suc x))) ≡⟨  cong (λ k → suc (nxn→n  (proj1 (n→nxn i)) (suc k))) (sym eq) ⟩
+          suc (nxn→n (proj1 (n→nxn i)) (suc (proj2  (n→nxn (suc i))))) ≡⟨  cong (λ k → suc (nxn→n  (proj1 (n→nxn i)) k)) ( begin
+              suc (proj2 (n→nxn (suc i))) ≡⟨ cong suc (cong proj2 (nid1 i nid7)) ⟩
+              suc (pred (proj2 (n→nxn i))) ≡⟨ nid6 nid7 ⟩
+              proj2 (n→nxn i) ∎ )⟩
+          suc (nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))) ≡⟨ cong suc (n-id i) ⟩ 
+          suc i ∎ where
+             open ≡-Reasoning
+             nid7 :  0 < proj2 (n→nxn i) 
+             nid7 = subst (λ k → 0 < k ) (sym eqy) (s≤s z≤n)
+             nid8 : suc (proj2  (n→nxn (suc i)))  ≡ proj2 (n→nxn i)
+             nid8 = begin
+                suc (proj2 (n→nxn (suc i))) ≡⟨ cong suc (cong proj2 (nid1 i nid7 )) ⟩
+                suc (pred (proj2 (n→nxn i))) ≡⟨ nid6 nid7 ⟩
+                proj2 (n→nxn i) ∎  
      f : (i : ℕ) → Set
      f i = n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫
      g : (i j : ℕ) → Set