{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}
module AFF2024.Algebra.AlgebraicallyClosedInfinite where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Algebra.CommRing
open import Data.List
open import Data.List.Relation.Unary.All

open import AFF2024.Basics
open import AFF2024.Algebra.Basics

module _ {ℓ : Level} (R…@(R , Rstr) : CommRing ℓ) where
  open CommRingStr Rstr
  open Apartness R…

  infinite : IsAlgebraicallyClosed R… → Infinite R _#_
  infinite = {!!}