--- a/src/HyperReal.agda	Fri Jul 02 12:39:52 2021 +0900
+++ b/src/HyperReal.agda	Fri Jul 02 17:21:27 2021 +0900
@@ -7,6 +7,7 @@
 open import Level renaming ( suc to succ ; zero to Zero )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Binary.Definitions
+open import Function.Bijection
 open import nat
 open import logic
 
@@ -20,6 +21,7 @@
      nn-id : (i j : ℕ) →  n→nxn (nxn→n ⟪ i , j ⟫ ) ≡ ⟪ i , j ⟫
      n-id : (i  : ℕ) →  nxn→n (n→nxn i ) ≡ i
 
+
 open _∧_
 
      -- t1 :  nxn→n 0 1 ≡ 1
@@ -91,8 +93,13 @@
 hzero : HyperNat
 hzero _ = 0 
 
-_n≤_ : (i j : HyperNat ) → Set -- ?
-i n≤ j = (k : ℕ ) → i k ≤ j k
+--
+--
+record _n≤_  (i j : HyperNat ) :  Set where 
+   field 
+      ≤-map : ℕ → ℕ
+      ≤-m : ℕ
+      is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (≤-map k)
 
 postulate
    _cmpn_  : ( i j : HyperNat ) → Dec ( i n≤ j )
@@ -118,9 +125,9 @@
 
 HNzero? : ( i : HyperNat ) → Dec (HNzero i)
 HNzero? i with i cmpn hzero | hzero cmpn i
-... | no s | t = no (λ n → s (λ k → subst (λ k → k ≤ 0) (sym (n k)) refl-≤ )) --  (k₁ : ℕ) → i k₁ ≡ 0  → i k ≤ 0
-... | s | no t = no (λ n → t (λ k → subst (λ k → 0 ≤ k) (sym (n k)) refl-≤ ))
-... | yes s | yes t = yes (λ k → ≤→= (s k) (t k))
+... | no s | t = no (λ n → s {!!}) --  (k₁ : ℕ) → i k₁ ≡ 0  → i k ≤ 0
+... | s | no t = no (λ n → t {!!})
+... | yes s | yes t = yes (λ k → {!!} )
 
 record HNzeroK ( x : HyperNat ) : Set where
   field