From dde5927315cc1f8cda50d92589d95fa6320052bc Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Thu, 14 Nov 2024 23:20:29 +0100
Subject: [PATCH 1/2] Prove essential lemma

---
 .../Polynomials/UnivariateList/Decidable.agda | 62 +++++++++++++++++++
 1 file changed, 62 insertions(+)
 create mode 100644 Cubical/Algebra/Polynomials/UnivariateList/Decidable.agda

diff --git a/Cubical/Algebra/Polynomials/UnivariateList/Decidable.agda b/Cubical/Algebra/Polynomials/UnivariateList/Decidable.agda
new file mode 100644
index 0000000000..4b4639e4fa
--- /dev/null
+++ b/Cubical/Algebra/Polynomials/UnivariateList/Decidable.agda
@@ -0,0 +1,62 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.Polynomials.UnivariateList.Decidable where
+
+{-
+Polynomials over commutative rings with decidable equality
+==========================================================
+-}
+
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Relation.Nullary.Base using (decRec; ¬_)
+open import Cubical.Relation.Nullary.DecidablePropositions
+
+open import Cubical.Data.Sigma
+open import Cubical.Data.Nat renaming (_+_ to _Nat+_; _·_ to _Nat·_) hiding (·-comm)
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Sum as Sum
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Bool hiding (_≤_)
+open import Cubical.HITs.PropositionalTruncation as PT
+
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.CommRing
+
+open import Cubical.Algebra.Polynomials.UnivariateList.Base
+
+private variable
+  ℓ : Level
+
+{-
+ if a sequence of decidable properties starting with a false one, becomes eventually true,
+ there is a highest natural number for which it is false
+-}
+lemma : (s : ℕ → DecProp ℓ)
+        → ¬ (s zero .fst .fst)
+        → ∃[ k ∈ ℕ ] ((l : ℕ) → k ≤ l → (s l) .fst .fst)
+        → Σ[ n ∈ ℕ ] ((¬ ((s n) .fst .fst)) × ((l : ℕ) → suc n ≤ l → (s l) .fst .fst))
+lemma s s-zero eventuallyHolds =
+  PT.rec isPropLatestCounterexamples
+         (λ {(k , p) → byInduction k p})
+         eventuallyHolds
+  where isPropLatestCounterexamples : isProp (Σ[ n ∈ ℕ ] ((¬ ((s n) .fst .fst)) × ((l : ℕ) → suc n ≤ l → (s l) .fst .fst)))
+        isPropLatestCounterexamples (n , p) (n' , p') =
+          Σ≡Prop (λ x → isProp× (isPropΠ (λ _ → isProp⊥)) (isPropΠ λ _ → isPropΠ λ _ → s _ .fst .snd))
+                 (≤CaseInduction {P = _≡_}
+                   (λ n≤n' → Sum.rec (λ suc-n≤n' → ⊥.rec ((p' .fst) (p .snd n' suc-n≤n') )) (λ n≡n' → n≡n') (≤-split n≤n'))
+                   (λ n'≤n → Sum.rec (λ suc-n'≤n → ⊥.rec ((p .fst) (p' .snd n suc-n'≤n))) sym (≤-split n'≤n)))
+
+        byInduction : (k' : ℕ) → ((l : ℕ) → k' ≤ l → (s l) .fst .fst)
+                      → Σ[ n ∈ ℕ ] ((¬ ((s n) .fst .fst)) × ((l : ℕ) → suc n ≤ l → (s l) .fst .fst))
+        byInduction zero    eventuallyHolds = zero , s-zero , λ l → λ 1≤l → eventuallyHolds l (≤-trans zero-≤ 1≤l)
+        byInduction (suc k) eventuallyHolds =
+          decRec (λ p →
+                    byInduction k
+                                (λ l k≤l → Sum.rec (λ k<l → eventuallyHolds l k<l)
+                                                   (λ k≡l → subst (λ l → s l .fst .fst) k≡l p)
+                                                   (≤-split k≤l)))
+                 (λ ¬p → k , ¬p , (λ l k+1≤l → eventuallyHolds l k+1≤l))
+                 (s k .snd)

From e07e8ad622d7a30acbee3ea5963d3d69c12bfa31 Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Thu, 14 Nov 2024 23:28:34 +0100
Subject: [PATCH 2/2] Fix comment

---
 Cubical/Algebra/Polynomials/UnivariateList/Decidable.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cubical/Algebra/Polynomials/UnivariateList/Decidable.agda b/Cubical/Algebra/Polynomials/UnivariateList/Decidable.agda
index 4b4639e4fa..579ce2d979 100644
--- a/Cubical/Algebra/Polynomials/UnivariateList/Decidable.agda
+++ b/Cubical/Algebra/Polynomials/UnivariateList/Decidable.agda
@@ -31,8 +31,8 @@ private variable
   ℓ : Level
 
 {-
- if a sequence of decidable properties starting with a false one, becomes eventually true,
- there is a highest natural number for which it is false
+ if a eventually true sequence of decidable propositions starts with a false propostion,
+ then there is a highest natural number for which it is false
 -}
 lemma : (s : ℕ → DecProp ℓ)
         → ¬ (s zero .fst .fst)