Updated code to check with Agda 2.6.2.2

viktorcsimma · viktorcsimma · commit c160f7dc236c · 2022-08-12T11:37:08.000+02:00
diff --git a/.agda-lib b/.agda-lib
@@ -0,0 +1,3 @@
+name: thesis
+depend: standard-library
+include: .
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1,2 @@
+/_build
+/*.agda~
diff --git a/ExtraProperties.agda b/ExtraProperties.agda
@@ -27,8 +27,10 @@ open import Algebra.Structures
 open import Data.Empty
 open import Data.Sum
 open import Data.Maybe.Base
+
 import NonReflectiveQ as ℚ-Solver
 import NonReflectiveZ as ℤ-Solver
+
 open import Data.List
 
 open ℚᵘ
@@ -300,3 +302,4 @@ p≤q+j⁻¹⇒p≤q {p} {q} hyp = p-q≤j⁻¹⇒p≤q (λ {(suc j-1) -> let j
   where
     open ℚP.≤-Reasoning
     open import NonReflectiveQ
+
diff --git a/Inverse.agda b/Inverse.agda
@@ -50,7 +50,11 @@ abstract
   not0-helper x x≄0 n = ℚP.p≄0⇒∣↥p∣≢0 xₛ (ℚ≠-helper xₛ ([ left , right ]′ (ℚP.∣p∣≡p∨∣p∣≡-p xₛ)))
     where
       open ℚP.≤-Reasoning
+
+      N : ℕ
       N = Nₐ x x≄0
+
+      xₛ : ℚᵘ
       xₛ = seq x ((n ℕ.+ N) ℕ.* (N ℕ.* N))
 
       0<∣xₛ∣ : 0ℚᵘ ℚ.< ℚ.∣ xₛ ∣
@@ -73,35 +77,59 @@ abstract
         ℚ.- ℚ.∣ xₛ ∣  <⟨ ℚP.neg-mono-< 0<∣xₛ∣ ⟩
         0ℚᵘ            ∎)
 
+
+--Had to declare separately as abstract in order to typecheck fast enough.
+--TODO: see whether it could be hidden from global scope.
+abstract
+  lesser-helper-2 : ∀ (x : ℝ) -> (x≄0 : x ≄0) -> ∀ (n : ℕ) -> (+ 1 / (Nₐ x x≄0)) ℚ.≤ ℚ.∣ seq x ((n ℕ.+ (Nₐ x x≄0)) ℕ.* ((Nₐ x x≄0) ℕ.* (Nₐ x x≄0))) ∣
+  lesser-helper-2 x x≄0 n = proj₂ (fast-lemma-2-8-1-if {∣ x ∣} (x≄0⇒pos∣x∣ {x} x≄0)) ((n ℕ.+ N) ℕ.* (N ℕ.* N)) lesser-helper
+    where
+    N : ℕ
+    N = Nₐ x x≄0
+    lesser-helper : (Nₐ x x≄0) ℕ.≤ (n ℕ.+ (Nₐ x x≄0)) ℕ.* ((Nₐ x x≄0) ℕ.* (Nₐ x x≄0))
+    lesser-helper = ℕP.≤-trans (ℕP.m≤n+m N n) (ℕP.m≤m*n (n ℕ.+ N) {N ℕ.* N} ℕP.0<1+n)
+
+
 abstract
   inverse-helper : ∀ (x : ℝ) -> (x≄0 : x ≄0) -> ∀ (n : ℕ) ->
                    ℚ.∣ (ℚ.1/ seq x ((n ℕ.+ (Nₐ x x≄0)) ℕ.* (Nₐ x x≄0 ℕ.* Nₐ x x≄0))) {not0-helper x x≄0 n} ∣ ℚ.≤ + (Nₐ x x≄0) / 1
   inverse-helper x x≄0 n = begin
     ℚ.∣ xₛ⁻¹ ∣                             ≈⟨ ℚP.≃-sym (ℚP.*-identityʳ ℚ.∣ xₛ⁻¹ ∣) ⟩
     ℚ.∣ xₛ⁻¹ ∣ ℚ.* 1ℚᵘ                     ≈⟨ ℚP.*-congˡ {ℚ.∣ xₛ⁻¹ ∣} (ℚP.≃-sym (ℚP.*-inverseˡ (+ N / 1))) ⟩
     ℚ.∣ xₛ⁻¹ ∣ ℚ.* (+ 1 / N ℚ.* (+ N / 1)) ≈⟨ ℚP.≃-sym (ℚP.*-assoc ℚ.∣ xₛ⁻¹ ∣ (+ 1 / N) (+ N / 1)) ⟩
-    ℚ.∣ xₛ⁻¹ ∣ ℚ.* (+ 1 / N) ℚ.* (+ N / 1) ≤⟨ ℚP.*-monoˡ-≤-nonNeg {+ N / 1} _ (ℚP.*-monoʳ-≤-nonNeg {ℚ.∣ xₛ⁻¹ ∣} _ lesser-helper-2) ⟩
+    ℚ.∣ xₛ⁻¹ ∣ ℚ.* (+ 1 / N) ℚ.* (+ N / 1) ≤⟨ ℚP.*-monoˡ-≤-nonNeg {+ N / 1} _ (ℚP.*-monoʳ-≤-nonNeg {ℚ.∣ xₛ⁻¹ ∣} (ℚ.nonNegative (ℚP.0≤∣p∣ (xₛ⁻¹))) (lesser-helper-2 x x≄0 n)) ⟩
     ℚ.∣ xₛ⁻¹ ∣ ℚ.* ℚ.∣ xₛ ∣ ℚ.* (+ N / 1)  ≈⟨ ℚP.*-congʳ {+ N / 1} helper ⟩
     1ℚᵘ ℚ.* (+ N / 1)                     ≈⟨ ℚP.*-identityˡ (+ N / 1) ⟩
     + N / 1                                 ∎
     where
       open ℚP.≤-Reasoning
+
+      N : ℕ
       N = Nₐ x x≄0
+
+      xₛ : ℚᵘ
       xₛ = seq x ((n ℕ.+ N) ℕ.* (N ℕ.* N))
+
+      xₛ≢0 : ℤ.∣ ↥ xₛ ∣ ≢0
       xₛ≢0 = not0-helper x x≄0 n
-      xₛ⁻¹ = (ℚ.1/ seq x ((n ℕ.+ N) ℕ.* (N ℕ.* N))) {xₛ≢0}
+  
+      
+      xₛ⁻¹ : ℚᵘ
+      xₛ⁻¹ = (ℚ.1/ xₛ) {xₛ≢0}
+      
 
       helper : ℚ.∣ xₛ⁻¹ ∣ ℚ.* ℚ.∣ xₛ ∣ ℚ.≃ ℚ.1ℚᵘ
       helper = begin-equality
         ℚ.∣ xₛ⁻¹ ∣ ℚ.* ℚ.∣ xₛ ∣ ≈⟨ ℚP.≃-sym (ℚP.∣p*q∣≃∣p∣*∣q∣ xₛ⁻¹ xₛ) ⟩
         ℚ.∣ xₛ⁻¹ ℚ.* xₛ ∣       ≈⟨ ℚP.∣-∣-cong (ℚP.*-inverseˡ xₛ {xₛ≢0}) ⟩
         ℚ.1ℚᵘ                    ∎
-
+{-
       lesser-helper : N ℕ.≤ (n ℕ.+ N) ℕ.* (N ℕ.* N)
       lesser-helper = ℕP.≤-trans (ℕP.m≤n+m N n) (ℕP.m≤m*n (n ℕ.+ N) {N ℕ.* N} ℕP.0<1+n)
 
-      lesser-helper-2 : + 1 / N ℚ.≤ ℚ.∣ xₛ ∣
+      lesser-helper-2 : (+ 1 / N) ℚ.≤ ℚ.∣ xₛ ∣
       lesser-helper-2 = proj₂ (fast-lemma-2-8-1-if {∣ x ∣} (x≄0⇒pos∣x∣ {x} x≄0)) ((n ℕ.+ N) ℕ.* (N ℕ.* N)) lesser-helper
+-}
 
 -- Definition of the multiplicative inverse function _⁻¹
 _⁻¹ : (x : ℝ) -> (x≄0 : x ≄ 0ℝ) -> ℝ
@@ -298,3 +326,4 @@ x<y∧posx,y⇒y⁻¹<x⁻¹ {x} {y} x<y x≄0 y≄0 posx posy = let x⁻¹ = (x
 ⁻¹-involutive-default : ∀ {x} -> (x≄0 : x ≄0) ->
                 (((x ⁻¹) x≄0) ⁻¹) ([ (λ x<0 -> inj₁ (x<0⇒x⁻¹<0 {x} x≄0 x<0)) , (λ 0<x -> inj₂ (0<x⇒0<x⁻¹ {x} x≄0 0<x))]′ x≄0) ≃ x
 ⁻¹-involutive-default {x} x≄0 = ⁻¹-involutive {x} x≄0 ([ (λ x<0 -> inj₁ (x<0⇒x⁻¹<0 {x} x≄0 x<0)) , (λ 0<x -> inj₂ (0<x⇒0<x⁻¹ {x} x≄0 0<x))]′ x≄0)
+
diff --git a/NonReflectiveQ.agda b/NonReflectiveQ.agda
@@ -15,3 +15,9 @@ isZero? p with 0ℚᵘ ≃? p
 
 open import Tactic.RingSolver.Core.AlmostCommutativeRing using (fromCommutativeRing)
 open import Tactic.RingSolver.NonReflective (fromCommutativeRing +-*-commutativeRing isZero?) public
+
+import Tactic.RingSolver.NonReflective
+import Data.Nat.Base as ℕ
+_⊖_ : {A : Set} → {n : ℕ.ℕ} → Tactic.RingSolver.NonReflective.Expr A n → Tactic.RingSolver.NonReflective.Expr A n → Tactic.RingSolver.NonReflective.Expr A n
+ex1 ⊖ ex2 = ex1 ⊕ (⊝ ex2)
+infixl 6 _⊖_
diff --git a/NonReflectiveZ.agda b/NonReflectiveZ.agda
@@ -0,0 +1,27 @@
+-- The nonreflective ring solver instantiated for integers.
+-- (could not find on the repository)
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Agda.Builtin.Bool
+open import Agda.Builtin.Equality
+open import Data.Maybe.Base using (Maybe; just; nothing)
+open import Relation.Nullary
+open import Data.Integer.Base as ℤ using (ℤ; +_; +0; +[1+_]; -[1+_])
+open import Data.Integer.Properties as ℤP
+open import Relation.Binary.Definitions
+
+isZero? : ∀ (p : ℤ) -> Maybe (ℤ.0ℤ ≡ p)
+isZero? p with ℤ.0ℤ ℤP.≟ p
+... | .true because ofʸ p₁ = just p₁
+... | .false because ofⁿ ¬p = nothing
+
+open import Tactic.RingSolver.Core.AlmostCommutativeRing using (fromCommutativeRing)
+open import Tactic.RingSolver.NonReflective (fromCommutativeRing +-*-commutativeRing isZero?) public
+
+import Tactic.RingSolver.NonReflective
+import Data.Nat.Base as ℕ
+_⊖_ : {A : Set} → {n : ℕ.ℕ} → Tactic.RingSolver.NonReflective.Expr A n → Tactic.RingSolver.NonReflective.Expr A n → Tactic.RingSolver.NonReflective.Expr A n
+ex1 ⊖ ex2 = ex1 ⊕ (⊝ ex2)
+infixl 6 _⊖_
+
diff --git a/RealProperties.agda b/RealProperties.agda
@@ -1704,8 +1704,11 @@ module ℝ-Solver where
     }
 
   abstract
+    ⋆-distrib-+₂ : ∀ (p r : ℚᵘ) -> (p ℚ.+ r) ⋆ ≃ p ⋆ + r ⋆
     ⋆-distrib-+₂   = ⋆-distrib-+
+    ⋆-distrib-*₂ : ∀ p q -> (p ℚ.* q) ⋆ ≃ p ⋆ * q ⋆
     ⋆-distrib-*₂   = ⋆-distrib-*
+    ⋆-distrib-neg₂ : ∀ (p : ℚᵘ) -> (ℚ.- p) ⋆ ≃ - (p ⋆)
     ⋆-distrib-neg₂ = ⋆-distrib-neg
 
   getMorphism : _-Raw-AlmostCommutative⟶_ ℚP.+-*-rawRing (fromCommutativeRing +-*-commutativeRing (λ x -> nothing))
@@ -2572,3 +2575,4 @@ x≤z∧y≤z⇒x⊔y≤z {x} {y} {z} x≤z y≤z = lemma-2-8-2-onlyif lem
                                                        (ℚP.-‿cong (ℚP.≃-sym (ℚP.p≤q⇒p⊔q≃q x₂ₘ≤y₂ₘ))) ⟩
           seq z (2 ℕ.* m) ℚ.- seq (x ⊔ y) (2 ℕ.* m)  ∎
 
+
diff --git a/Sequence.agda b/Sequence.agda
@@ -562,26 +562,36 @@ nonNegx∧x≄0⇒posx {x} nonx x≄0 = 0<x⇒posx (begin-strict
 nonNegx⇒nonNegx⁻¹ : ∀ {x} -> NonNegative x -> (x≄0 : x ≄0) -> NonNegative ((x ⁻¹) x≄0)
 nonNegx⇒nonNegx⁻¹ {x} nonx x≄0 = pos⇒nonNeg (posx⇒posx⁻¹ {x} x≄0 (nonNegx∧x≄0⇒posx {x} nonx x≄0))
 
+
 abstract
   xₙ≄0∧x₀≄0⇒xₙ⁻¹→x₀⁻¹ : ∀ {xs : ℕ -> ℝ} -> ∀ {x₀ : ℝ} -> xs ConvergesTo x₀ -> (xₙ≄0 : ∀ n -> xs n ≄0) -> (x₀≄0 : x₀ ≄0) ->
                         (λ n -> (xs n ⁻¹) (xₙ≄0 n)) ConvergesTo (x₀ ⁻¹) x₀≄0
   xₙ≄0∧x₀≄0⇒xₙ⁻¹→x₀⁻¹ {xs} {x₀} (con* xₙ→x₀) xₙ≄0 x₀≄0 = con* main
+    
     where
       open ≤-Reasoning
       main : ∀ k -> {k≢0 : k ≢0} -> ∃ λ N-1 -> ∀ n -> n ℕ.≥ suc N-1 ->
              ∣ (xs n ⁻¹) (xₙ≄0 n) - (x₀ ⁻¹) x₀≄0 ∣ ≤ ((+ 1 / k) {k≢0}) ⋆
       main (suc k-1) = ℕ.pred N , sub
+      
         where
+          arch : ∃ (λ n-1 → (mkℚᵘ (+ 1) n-1 ⋆ < (+ 1 / 2) ⋆ * ∣ x₀ ∣)) --had to add this
           arch = fast-archimedean-ℝ₂ {(+ 1 / 2) ⋆ * ∣ x₀ ∣} (posx,y⇒posx*y (posp⇒posp⋆ (+ 1 / 2) _) (x≄0⇒pos∣x∣ x₀≄0))
+          
+          r k : ℕ
           r = suc (proj₁ arch)
           k = suc k-1
+
+          m₀-getter : ∃ (λ N-1 → (n : ℕ) → n ℕ.≥ suc N-1 → ∣ xs n - x₀ ∣ < ((+ 1 / (2 ℕ.* (suc k-1))) ⋆ * (∣ x₀ ∣ * ∣ x₀ ∣))) --had to add this too
           m₀-getter = fast-ε-from-convergence (x₀ , con* xₙ→x₀) ((+ 1 / (2 ℕ.* k)) ⋆ * (∣ x₀ ∣ * ∣ x₀ ∣))
                       (posx,y⇒posx*y (posp⇒posp⋆ (+ 1 / (2 ℕ.* k)) _)
                       (posx,y⇒posx*y (x≄0⇒pos∣x∣ x₀≄0) (x≄0⇒pos∣x∣ x₀≄0)))
+          
+          m₀ n₀ N : ℕ
           m₀ = suc (proj₁ m₀-getter)
           n₀ = suc (proj₁ (xₙ→x₀ r))
           N = m₀ ℕ.⊔ n₀
-
+          
           {-
             [1]
             Incredible optimization note!
@@ -593,7 +603,7 @@ abstract
             Despite this issue being solved, the addition of all of the implicit arguments below is a notable optimization, and will
             thus be kept.
           -}
-          sub : ∀ n -> n ℕ.≥ N -> ∣ (xs n ⁻¹) (xₙ≄0 n) - (x₀ ⁻¹) x₀≄0 ∣ ≤ (+ 1 / k) ⋆
+          sub : ∀ n -> n ℕ.≥ N -> ∣ (xs n ⁻¹) (xₙ≄0 n) - (x₀ ⁻¹) x₀≄0 ∣ ≤ (+ 1 / suc k-1) ⋆
           sub n n≥N = begin
             ∣ xₙ⁻¹ - x₀⁻¹ ∣                          ≈⟨ ≃-trans {∣ xₙ⁻¹ - x₀⁻¹ ∣} {∣xₙ∣⁻¹ * ∣x₀∣⁻¹ * ∣ x₀ - xₙ ∣} {∣ x₀ - xₙ ∣ * (∣xₙ∣⁻¹ * ∣x₀∣⁻¹)}
                                                         part2 (*-comm (∣xₙ∣⁻¹ * ∣x₀∣⁻¹) ∣ x₀ - xₙ ∣) ⟩
@@ -626,16 +636,24 @@ abstract
                                                           ℤΚ (+ 1) :* ℤΚ (+ 2) :* k := ℤΚ (+ 1) :* (ℤΚ (+ 2) :* k :* ℤΚ (+ 1)))
                                                           refl (+ k))) ⟩
             (+ 1 / k) ⋆                                 ∎
-          
+           
+            
             where
+              --maybe the main problem was here; it hung until the types were added
+              xₙ xₙ⁻¹ x₀⁻¹ : ℝ
               xₙ = xs n
               xₙ⁻¹ = (xₙ ⁻¹) (xₙ≄0 n)
               x₀⁻¹ = (x₀ ⁻¹) x₀≄0
+
+              ∣xₙ∣≄0 : ∣ xₙ ∣ ≄0
               ∣xₙ∣≄0 = x≄0⇒∣x∣≄0 (xₙ≄0 n)
+              ∣x₀∣≄0 : ∣ x₀ ∣ ≄0
               ∣x₀∣≄0 = x≄0⇒∣x∣≄0 x₀≄0
+              
+              ∣xₙ∣⁻¹ ∣x₀∣⁻¹ : ℝ
               ∣xₙ∣⁻¹ = (∣ xₙ ∣ ⁻¹) ∣xₙ∣≄0
               ∣x₀∣⁻¹ = (∣ x₀ ∣ ⁻¹) ∣x₀∣≄0
-
+              
               2⁻¹∣x₀∣<∣xₙ∣ : (+ 1 / 2) ⋆ * ∣ x₀ ∣ < ∣ xₙ ∣
               2⁻¹∣x₀∣<∣xₙ∣ = begin-strict
                 (+ 1 / 2) ⋆ * ∣ x₀ ∣            ≈⟨ solve 1 (λ ∣x₀∣ ->
@@ -650,7 +668,7 @@ abstract
                                                    x₀ ⊖ (x₀ ⊖ xₙ) ⊜ xₙ)
                                                    ≃-refl xₙ x₀) ⟩
                 ∣ xₙ ∣                          ∎
-
+              
               part1 : xₙ⁻¹ - x₀⁻¹ ≃ xₙ⁻¹ * x₀⁻¹ * (x₀ - xₙ)
               part1 = ≃-symm (begin-equality
                 xₙ⁻¹ * x₀⁻¹ * (x₀ - xₙ)                 ≈⟨ *-distribˡ-+ (xₙ⁻¹ * x₀⁻¹) x₀ (- xₙ) ⟩
@@ -667,7 +685,7 @@ abstract
                                                            (+-congʳ xₙ⁻¹ (*-congˡ { - x₀⁻¹} (*-inverseˡ xₙ (xₙ≄0 n)))))
                                                            (+-congʳ xₙ⁻¹ (*-identityʳ (- x₀⁻¹))) ⟩
                 xₙ⁻¹ - x₀⁻¹                              ∎)
-
+              
               part2 : ∣ xₙ⁻¹ - x₀⁻¹ ∣ ≃ ∣xₙ∣⁻¹ * ∣x₀∣⁻¹ * ∣ x₀ - xₙ ∣
               part2 = begin-equality
                 ∣ xₙ⁻¹ - x₀⁻¹ ∣                   ≈⟨ ∣-∣-cong part1 ⟩
@@ -677,7 +695,7 @@ abstract
                                                     (∣x∣⁻¹≃∣x⁻¹∣ {xₙ} ∣xₙ∣≄0 (xₙ≄0 n))
                                                     (∣x∣⁻¹≃∣x⁻¹∣ {x₀} ∣x₀∣≄0 x₀≄0))) ⟩
                 ∣xₙ∣⁻¹ * ∣x₀∣⁻¹ * ∣ x₀ - xₙ ∣      ∎
-
+              
               part3 : ∣xₙ∣⁻¹ < 2ℚᵘ ⋆ * ∣x₀∣⁻¹
               part3 = let 2⁻¹≄0 = ∣↥p∣≢0⇒p⋆≄0 (+ 1 / 2) _
                                 ; 2⁻¹∣x₀∣≄0 = x≄0∧y≄0⇒x*y≄0 {(+ 1 / 2) ⋆} {∣ x₀ ∣} 2⁻¹≄0 ∣x₀∣≄0 in begin-strict
@@ -690,7 +708,7 @@ abstract
                     (((+ 1 / 2) ⋆) ⁻¹) 2⁻¹≄0 * ∣x₀∣⁻¹                ≈⟨ *-congʳ {∣x₀∣⁻¹} (⋆-distrib-⁻¹ (+ 1 / 2) 2⁻¹≄0) ⟩
                     2ℚᵘ ⋆ * ∣x₀∣⁻¹                                    ∎
 
-              part4 : ∣ x₀ - xₙ ∣ < (+ 1 / (2 ℕ.* k)) ⋆ * (∣ x₀ ∣ * ∣ x₀ ∣)
+              part4 : ∣ x₀ - xₙ ∣ < (+ 1 / (2 ℕ.* (suc k-1))) ⋆ * (∣ x₀ ∣ * ∣ x₀ ∣)
               part4 = begin-strict
                 ∣ x₀ - xₙ ∣                             ≈⟨ ∣x-y∣≃∣y-x∣ x₀ xₙ ⟩
                 ∣ xₙ - x₀ ∣                             <⟨ proj₂ m₀-getter n (ℕP.≤-trans (ℕP.m≤m⊔n m₀ n₀) n≥N) ⟩
@@ -2345,12 +2363,21 @@ Order Limit Theorem
 -}
 0≤xₙ⇒0≤limxₙ : {xs : ℕ → ℝ} → ((n : ℕ) → 0ℝ ≤ xs n) → (xₙ→x : xs isConvergent)  → 0ℝ ≤ lim xₙ→x
 0≤xₙ⇒0≤limxₙ {xs} 0≤xₙ xₙ→x = ≮⇒≥ λ x<0 → <-irrefl ≃-refl
-                              let x = lim xₙ→x; N-get = (fast-ε-from-convergence xₙ→x (- x) (0<x⇒posx (<-respˡ-≃ (≃-symm 0≃-0) (neg-mono-< x<0))))
-                                    ; N = suc (proj₁ N-get) in begin-strict
-  - x      ≤⟨ ≤-respˡ-≃ (+-identityˡ (- x)) (+-monoˡ-≤ (- x) (0≤xₙ N))  ⟩
-  xs N - x <⟨ ≤-<-trans x≤∣x∣ (proj₂ N-get N ℕP.≤-refl) ⟩
-  - x       ∎
-  where open ≤-Reasoning
+                              (begin-strict
+  - x                  ≤⟨ ≤-respˡ-≃ (+-identityˡ (- x)) (+-monoˡ-≤ (- x) (0≤xₙ N)) ⟩
+  xs (N {x<0}) - x     <⟨ ≤-<-trans x≤∣x∣ (proj₂ N-get N ℕP.≤-refl) ⟩
+  - x       ∎)
+  where
+    open ≤-Reasoning
+
+    x : ℝ
+    x = lim xₙ→x
+
+    N-get : {x<0 : x < 0ℝ} → ∃ (λ N-1 → (n : ℕ) → n ℕ.≥ suc N-1 → ∣ xs n - x ∣ < - x)
+    N-get {x<0} = fast-ε-from-convergence xₙ→x (- x) (0<x⇒posx (<-respˡ-≃ (≃-symm 0≃-0) (neg-mono-< x<0)))
+
+    N : {x<0 : x < 0ℝ} → ℕ
+    N {x<0} = suc (proj₁ (N-get {x<0}))
 
 xₙ≤yₙ⇒limxₙ≤limyₙ : {xs ys : ℕ → ℝ} → ((n : ℕ) → xs n ≤ ys n) → (xₙ→x : xs isConvergent) (yₙ→y : ys isConvergent) → lim xₙ→x ≤ lim yₙ→y
 xₙ≤yₙ⇒limxₙ≤limyₙ {xs} {ys} xₙ≤yₙ xₙ→x yₙ→y = 0≤y-x⇒x≤y (0≤xₙ⇒0≤limxₙ {λ n → ys n - xs n} (λ n → x≤y⇒0≤y-x (xₙ≤yₙ n))
@@ -2457,3 +2484,4 @@ abstract
                             (k : ℕ) {k≢0 : k ≢0} → ∃ λ Nₖ-1 → (n : ℕ) → n ℕ.≥ suc Nₖ-1 →
                             ∣ xs n - lim xₙ→x ∣ ≤ ((+ 1 / k) {k≢0}) ⋆
   fast-convergence-getter = convergence-getter
+

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+name: thesis`
	`2`	`+depend: standard-library`
	`3`	`+include: .`