RealRooted.lean

import RealRooted.ASWCubicCharacteristic
import RealRooted.ASWCubicClosedForm
import RealRooted.ASWCubicClosedFormAdapter
import RealRooted.ASWCubicDegreeThree
import RealRooted.ASWCubicDominance
import RealRooted.ASWCubicEqualModulus
import RealRooted.ASWCubicMinors
import RealRooted.ASWCubicNonrealFactor
import RealRooted.ASWCubicRecurrence
import RealRooted.ASWKarlinKernel
import RealRooted.ASWKarlinMatrix
import RealRooted.ASWKarlinSineBounds
import RealRooted.ASWKarlinThreshold
import RealRooted.ASWKarlinVariation
import RealRooted.ASWKarlinVectors
import RealRooted.AffineDerivative
import RealRooted.AffineFamily
import RealRooted.AffineFamily.Basic
import RealRooted.AffineFamily.Boundary
import RealRooted.AffineFamily.LowDegree
import RealRooted.AffineFamily.PositiveFamily
import RealRooted.AffineFamily.RootCrossing
import RealRooted.AffineFamily.Wronskian
import RealRooted.AffineLineRestriction
import RealRooted.AffineProperPosition
import RealRooted.AissenSchoenbergWhitney
import RealRooted.AissenSchoenbergWhitneyBase
import RealRooted.AllCombo
import RealRooted.Apolarity
import RealRooted.Applications.EulerianVariations
import RealRooted.Applications.EulerianVariations.CyclicPathDescents
import RealRooted.Applications.EulerianVariations.PeakValues
import RealRooted.Applications.EulerianVariations.TernaryRuns
import RealRooted.Applications.EulerianVariations.TernaryRuns.Recurrence
import RealRooted.Analysis.PowerTail
import RealRooted.Analysis.PowerTail.Bernoulli
import RealRooted.Analysis.PowerTail.Quadratic
import RealRooted.Analysis.PowerTail.Telescoping
import RealRooted.ArrayPolynomialDeterminant
import RealRooted.ArrayPolynomialDeterminantIdentification
import RealRooted.ArrayPolynomialDeterminantRecurrence
import RealRooted.ArrayPolynomialSchur
import RealRooted.ArrayPolynomialWeights
import RealRooted.Basic
import RealRooted.Basic.AffineInterlacing
import RealRooted.Basic.Coefficients
import RealRooted.Basic.Coefficients.Multivariate
import RealRooted.Basic.IntervalInequalities
import RealRooted.Basic.PolynomialFacts
import RealRooted.Basic.ProperPosition
import RealRooted.Basic.RootLists
import RealRooted.BasisTransform
import RealRooted.Bezoutian
import RealRooted.Bezoutian.ComplexRoots
import RealRooted.Bezoutian.LowDegree
import RealRooted.Bezoutian.MatrixBasics
import RealRooted.Bezoutian.RootEvaluation
import RealRooted.Bezoutian.StrictInterleaving
import RealRooted.Bezoutian.WronskianConverse
import RealRooted.BivariateOpenMapping
import RealRooted.BrandenLeite.ChainPolynomial
import RealRooted.BrandenLeite.ChainPolynomial.Algebra
import RealRooted.BrandenLeite.ChainPolynomial.Resolution
import RealRooted.BrandenLeite.Network
import RealRooted.BrandenLeite.NetworkTotallyNonneg
import RealRooted.BrandenLeite.NetworkWhitney
import RealRooted.BrandenVecchi.Chow
import RealRooted.BrandenLeite.Resolvable
import RealRooted.BrandenLeite.ResolvableTotallyNonneg
import RealRooted.BrandenLeite.Theorem37
import RealRooted.BrandenLeite.WhitneyReduction
import RealRooted.BorceaBranden.Applications.AffineFiniteSymbol
import RealRooted.BorceaBranden.Applications.BidiagonalSymbol
import RealRooted.BorceaBranden.Applications.BidiagonalSymbol.RealConsequences
import RealRooted.BorceaBranden.Applications.ComplexClassification
import RealRooted.BorceaBranden.Applications.ComplexUnivariateSymbol
import RealRooted.BorceaBranden.Applications.DegreeBoxPolarization
import RealRooted.BorceaBranden.Applications.EulerFiniteSymbol
import RealRooted.BorceaBranden.Applications.GeneralDegreeBoxPolarization
import RealRooted.BorceaBranden.Applications.GeneralDegreeBoxPolarization.CoefficientExtraction
import RealRooted.BorceaBranden.Applications.GeneralDegreeBoxPolarization.Derivative
import RealRooted.BorceaBranden.Applications.HarmonicSubstitution
import RealRooted.BorceaBranden.Applications.HarmonicSubstitution.BFJAuxiliary
import RealRooted.BorceaBranden.Applications.HarmonicSubstitution.BFJAuxiliary.Homogeneous
import RealRooted.BorceaBranden.Applications.HarmonicSubstitution.BFJOutput
import RealRooted.BorceaBranden.Applications.HarmonicSubstitution.BFJOutput.PFHomogenize
import RealRooted.BorceaBranden.Applications.HarmonicSubstitution.BFJOutput.PolyaFrequency
import RealRooted.BorceaBranden.Applications.HarmonicSubstitution.BFJOutput.Product
import RealRooted.BorceaBranden.Applications.HarmonicSubstitution.BFJOutput.Stability
import RealRooted.BorceaBranden.Applications.HomogenizeStable
import RealRooted.BorceaBranden.Applications.RealUnivariateSymbol
import RealRooted.BorceaBranden.Applications.RealUnivariateSymbol.Interlacing
import RealRooted.BorceaBranden.Applications.UnivariateSymbol
import RealRooted.BorceaBranden.BoundarySpecialization
import RealRooted.BorceaBranden.FiniteSymbolBasis
import RealRooted.BorceaBranden.FiniteSymbolClassification
import RealRooted.BorceaBranden.FiniteSymbolCoefficient
import RealRooted.BorceaBranden.FiniteSymbolContraction
import RealRooted.BorceaBranden.FiniteSymbolDegree
import RealRooted.BorceaBranden.FiniteSymbolLinearity
import RealRooted.BorceaBranden.FiniteSymbolPreserver
import RealRooted.BorceaBranden.FiniteSymbolProduct
import RealRooted.BorceaBranden.FiniteSymbolReciprocal
import RealRooted.BorceaBranden.FiniteSymbolReconstruction
import RealRooted.BorceaBranden.FiniteSymbolReconstructionCore
import RealRooted.BorceaBranden.UnivariateFiniteSymbol
import RealRooted.BoundarySpecializationGeneral
import RealRooted.BoundarySpecializationRight
import RealRooted.CauchyInterlacing
import RealRooted.CauchyInterlacing.Polynomial
import RealRooted.ClassicalHurwitzMatrix
import RealRooted.ClassicalHurwitzMatrix.Routh
import RealRooted.ClassicalHurwitzMatrix.Routh.Determinant
import RealRooted.ClassicalHurwitzMatrix.Routh.ReverseTotallyNonnegative
import RealRooted.ClassicalHurwitzMatrix.Routh.Sequence
import RealRooted.ClassicalHurwitzMatrix.Routh.Sequence.TotallyNonnegative
import RealRooted.ClassicalHurwitzMatrix.Routh.TotallyNonnegative
import RealRooted.ClassicalHurwitzMatrix.Stability
import RealRooted.ClassicalHurwitzMatrix.Stability.ClosedLimit
import RealRooted.ClassicalHurwitzMatrix.Stability.Closure
import RealRooted.ClassicalHurwitzMatrix.Stability.Converse
import RealRooted.ClassicalHurwitzMatrix.Stability.Criterion
import RealRooted.ClassicalHurwitzMatrix.Stability.Extraction
import RealRooted.ClassicalHurwitzMatrix.Stability.HermiteBiehler
import RealRooted.ClassicalHurwitzMatrix.Stability.Parity
import RealRooted.ClassicalHurwitzMatrix.Stability.Rotation
import RealRooted.ClassicalHurwitzMatrix.Stability.Routh
import RealRooted.ClassicalHurwitzMatrix.Stability.Routh.ProperPosition
import RealRooted.ClassicalHurwitzMatrix.Stability.Routh.Reverse
import RealRooted.ClassicalHurwitzMatrix.Stability.Routh.Sequence
import RealRooted.ClassicalHurwitzMatrix.Stability.Routh.WeakReverse
import RealRooted.ClassicalHurwitzMatrix.Stability.Terminal
import RealRooted.ClassicalHurwitzMatrix.Stability.Vieta
import RealRooted.ClassicalHurwitzMatrix.Stability.WeakConverse
import RealRooted.ClassicalHurwitzMatrix.TotallyNonnegative
import RealRooted.Challenges.AissenSchoenbergWhitney
import RealRooted.Challenges.BorceaBranden
import RealRooted.Challenges.BrandenSolus
import RealRooted.Challenges.BraunJal
import RealRooted.Challenges.CauchyInterlacing
import RealRooted.Challenges.ChudnovskySeymour
import RealRooted.Challenges.Eulerian
import RealRooted.Challenges.Favard
import RealRooted.Challenges.Hadamard
import RealRooted.Challenges.HermiteBiehlerHurwitz
import RealRooted.Challenges.HermitePoulain
import RealRooted.Challenges.HosterStump
import RealRooted.Challenges.Issue34SingleMatrixCounterexample
import RealRooted.Challenges.Issue34WindowObstruction
import RealRooted.Challenges.Kurtz
import RealRooted.Challenges.MatrixInterlacing
import RealRooted.Challenges.Obreschkoff
import RealRooted.Challenges.OperatorPreservers
import RealRooted.Challenges.VeroneseSections
import RealRooted.Challenges.Wagner
import RealRooted.ChudnovskySeymour
import RealRooted.ChudnovskySeymour.Core
import RealRooted.ChudnovskySeymour.Reductions
import RealRooted.ClosedSegmentCountEqFromAnalytic
import RealRooted.CoefficientDominance
import RealRooted.CoefficientDominance.LogConcavity
import RealRooted.CoefficientDominance.RootGap
import RealRooted.CoefficientDominance.Sequence
import RealRooted.CoefficientDominance.Symmetric
import RealRooted.CoefficientDominance.Symmetric.Finite
import RealRooted.CoefficientDominance.Symmetric.Polynomial
import RealRooted.CoefficientDominance.Symmetric.Sharp
import RealRooted.CoefficientDominance.Symmetric.Tail
import RealRooted.CoefficientDominance.Symmetric.Upper
import RealRooted.CoefficientShape
import RealRooted.CombinatorialExamples
import RealRooted.CombinatorialExamples.BigDescentsOddBinom
import RealRooted.CombinatorialExamples.ColoredSetPartitions
import RealRooted.CombinatorialExamples.Common
import RealRooted.CombinatorialExamples.Eulerian
import RealRooted.CombinatorialExamples.Motzkin
import RealRooted.CombinatorialExamples.Narayana
import RealRooted.CombinatorialExamples.OneDescentGamma
import RealRooted.CombinatorialExamples.PeakValues
import RealRooted.CombinatorialExamples.PeakValues.Insertion
import RealRooted.CombinatorialExamples.PeakValues.InsertionSum
import RealRooted.CombinatorialExamples.PeakValues.Sharpness
import RealRooted.CombinatorialExamples.PeakValues.Stability
import RealRooted.CombinatorialExamples.PeakValues.TranslatedRecurrence
import RealRooted.CombinatorialExamples.PeakValues.WeightedInterleaving
import RealRooted.CombinatorialExamples.Simsun
import RealRooted.CombinatorialExamples.SingletonFreeSetPartitions
import RealRooted.CombinatorialExamples.StirlingPermutations
import RealRooted.CombinatorialExamples.SturmDerangementsExc
import RealRooted.CombinatorialExamples.Touchard
import RealRooted.CombinatorialExamples.TypeBEulerian
import RealRooted.Combinatorics.OrderedSubsetPairsNarayana
import RealRooted.CommonInterleaver.AffineBoundary
import RealRooted.CommonInterleaver.DescPolynomial
import RealRooted.CommonInterleaver.FamilyUpgrade
import RealRooted.CommonInterleaver.Finite
import RealRooted.CommonInterleaver.IntervalLemmas
import RealRooted.CommonInterleaver.PairBridge
import RealRooted.CommonInterleaver.PairBridge.Compatibility
import RealRooted.CommonInterleaver.PairBridge.Compatibility.NonnegativeShift
import RealRooted.CommonInterleaver.PairBridge.Forward
import RealRooted.CommonInterleaver.PairBridge.Reduction
import RealRooted.CommonInterleaver.PairBridge.Reduction.AllCombo
import RealRooted.CommonInterleaver.PairBridge.Reduction.Basic
import RealRooted.CommonInterleaver.PairBridge.Reduction.CommonInterleaver
import RealRooted.CommonInterleaver.PairBridge.Reduction.CommonRoot
import RealRooted.CommonInterleaver.PairBridge.SuccDegree
import RealRooted.CommonInterleaver.PairBridge.SuccDegree.ClosedSegment
import RealRooted.CommonInterleaver.PairBridge.SuccDegree.RootCount
import RealRooted.CommonInterleaver.PairBridge.SuccDegree.RootCrossing
import RealRooted.CommonInterleaver.PairBridge.SuccDegree.SlotData
import RealRooted.CommonInterleaver.PairwiseUpgrade
import RealRooted.CommonInterleaver.PairwiseUpgrade.FamilyCompatibility
import RealRooted.CommonInterleaver.PairwiseUpgrade.FourWay
import RealRooted.CommonInterleaver.PairwiseUpgrade.FourWay.Equivalences
import RealRooted.CommonInterleaver.PairwiseUpgrade.LowDegree
import RealRooted.CommonInterleaver.RightPencil
import RealRooted.CommonInterleaver.RootDesc
import RealRooted.CommonInterleaver.RootCountCombinatorics
import RealRooted.CommonInterleaver.RootSelection
import RealRooted.CommonInterleaver.RootSelectionExamples
import RealRooted.CommonInterleaver.RootSelectionTree
import RealRooted.CommonInterleaver.RootSlots
import RealRooted.CommonInterleaver.RootSlots.Basic
import RealRooted.CommonInterleaver.Sequence
import RealRooted.CommonInterleaver.SameDegreeRootCount
import RealRooted.CommonInterleaver.Statements
import RealRooted.CommonInterleaver.SuccDegreeEndpoint
import RealRooted.CommonInterleaver.SuccDegreeLowDegree
import RealRooted.CommonInterleaverFamilySum
import RealRooted.CommonInterleaverExamples
import RealRooted.CommonInterleaverSeq
import RealRooted.CommonInterleaverTwo
import RealRooted.Compatibility.Basic
import RealRooted.Compatibility.InterleaverBridge
import RealRooted.Compatibility.Pair
import RealRooted.Compatibility.Three
import RealRooted.ComplexCesaro
import RealRooted.ComplexPowers
import RealRooted.ConvexCombination
import RealRooted.CubicDiscriminant
import RealRooted.CubicNewton
import RealRooted.DegreeDropDivXPrec
import RealRooted.DegreeDropReversal
import RealRooted.DegreeIncreasingLocalLowerCount
import RealRooted.Derivative
import RealRooted.Derivative.Algebra
import RealRooted.Derivative.FamilyClosure
import RealRooted.Derivative.Interlacing
import RealRooted.Derivative.LinearCombination
import RealRooted.Derivative.RootCounting
import RealRooted.DerivativeRecurrence
import RealRooted.DerivativeRecurrence.Linear
import RealRooted.DerivativeRecurrence.QuadraticDegree
import RealRooted.DerivativeRecurrence.GeneralizedLaguerre
import RealRooted.DerivativeRecurrence.GeneralizedLaguerreInterlacing
import RealRooted.DerivativeRecurrence.QuadraticInterlacing
import RealRooted.DerivativeRecurrence.QuadraticSeed
import RealRooted.DerivativeRecurrence.QuadraticShift
import RealRooted.DerivativeRecurrence.SecondOrderDegree
import RealRooted.DerivativeRecurrence.SecondOrderInterlacing
import RealRooted.DerivativeRecurrence.SecondDerivativeDegree
import RealRooted.DerivativeShiftRootMatching
import RealRooted.DerivativeShiftSequence
import RealRooted.DeterminantalStability
import RealRooted.DifferentialBlocks
import RealRooted.ElementaryDifferential
import RealRooted.EndpointDerivative
import RealRooted.EndpointDerivative.Basic
import RealRooted.EndpointDerivative.Sequence
import RealRooted.EulerOperator
import RealRooted.EulerOperator.Darboux
import RealRooted.EulerOperator.Darboux.Basic
import RealRooted.EulerOperator.Darboux.Interlacing
import RealRooted.EulerOperator.Pencil
import RealRooted.EulerOperator.OrderNumerator.Basic
import RealRooted.EulerOperator.OrderNumerator.Preservation
import RealRooted.EulerOperator.Polar
import RealRooted.EulerOperator.Polar.MultiplierSequence
import RealRooted.EulerOperator.Polar.Pencil
import RealRooted.EulerOperator.Polar.ProperPosition
import RealRooted.EulerOperator.ScaledPolar
import RealRooted.EulerOperator.Shift
import RealRooted.EulerianCompletion
import RealRooted.EulerianMixedCompatibility
import RealRooted.EulerianMixedCompatibility.Insertion
import RealRooted.Favard
import RealRooted.Favard.Affine
import RealRooted.Favard.Affine.Basic
import RealRooted.Favard.Affine.Denominator
import RealRooted.Favard.Affine.RowSign
import RealRooted.Favard.Orthogonality
import RealRooted.Favard.Recurrence
import RealRooted.FiniteFreeAdditive
import RealRooted.FiniteFreeAdditive.HalfInteger
import RealRooted.FiniteFreeAdditive.HalfIntegerConvolution
import RealRooted.FiniteFreeAdditive.HalfIntegerPreservation
import RealRooted.FiniteFreeAdditiveIdentity
import RealRooted.FiniteFreeAdditivePreservation
import RealRooted.FiniteFreeMultiplicative
import RealRooted.FiniteFreeRootCount
import RealRooted.FolkloreLemma
import RealRooted.GammaRealRoots
import RealRooted.GammaTransform
import RealRooted.GammaTransform.Basic
import RealRooted.GammaTransform.ProperPosition
import RealRooted.GammaTransform.Preservation
import RealRooted.GammaTransform.RootLists
import RealRooted.GammaTransform.RootMap
import RealRooted.GarloffWagner
import RealRooted.GarloffWagner.Algebra
import RealRooted.GarloffWagner.Iterated
import RealRooted.GarloffWagner.KreinData
import RealRooted.GarloffWagner.KreinExpansion
import RealRooted.GarloffWagner.Theorem12
import RealRooted.GarloffWagner.Hadamard
import RealRooted.GeneralizedEulerian
import RealRooted.GeneralizedLiuWang
import RealRooted.GeneralizedSnakePosets
import RealRooted.GeneralizedSnakePosets.FiniteBoard
import RealRooted.GeneralizedSnakePosets.MatrixInduction
import RealRooted.GeneralizedSnakePosets.Narayana.Claim7
import RealRooted.GeneralizedSnakePosets.Narayana.Claim7Analytic
import RealRooted.GeneralizedSnakePosets.Narayana.JacobiTransport
import RealRooted.GeneralizedSnakePosets.Narayana.LowRank
import RealRooted.GeneralizedSnakePosets.Narayana.Modified
import RealRooted.GeneralizedSnakePosets.Narayana.PFFacts
import RealRooted.GeneralizedSnakePosets.Narayana.RankSix
import RealRooted.GeneralizedSnakePosets.Narayana.Recurrence
import RealRooted.GeneralizedSnakePosets.Narayana.RootSums
import RealRooted.GeneralizedSnakePosets.Narayana.Turan
import RealRooted.GeneralizedSnakePosets.Narayana.TuranCertificates
import RealRooted.GeneralizedSnakePosets.Section3Packages
import RealRooted.GeneralizedSnakePosets.SnakeBoard
import RealRooted.GeneralizedSnakePosets.SnakeCover
import RealRooted.GeneralizedSnakePosets.SnakeReachability
import RealRooted.GeneralizedSnakePosets.SnakeStaircase
import RealRooted.GeneralizedSnakePosets.SnakeWord
import RealRooted.GeneralizedSnakePosets.SquarecaseModel
import RealRooted.GeneralizedSnakePosets.Statements
import RealRooted.GeneralizedSnakePosets.TruncatedStaircase
import RealRooted.GeneralizedSnakePosets.TruncatedStaircase.Auxiliary
import RealRooted.GeneralizedSnakePosets.TruncatedStaircase.Basic
import RealRooted.GeneralizedSnakePosets.TruncatedStaircase.BottomRow
import RealRooted.GeneralizedSnakePosets.TruncatedStaircase.FiniteCases
import RealRooted.GeneralizedSnakePosets.TruncatedStaircase.FullStaircase
import RealRooted.GeneralizedSnakePosets.TruncatedStaircase.RowFormulas
import RealRooted.GeneralizedSnakePosetsNarayana
import RealRooted.Graph.ClawFree
import RealRooted.Graph.AcyclicOrientation
import RealRooted.Graph.ChordalAcyclicSink
import RealRooted.Graph.AllOrientationSink
import RealRooted.Graph.IndependencePolynomial.Basic
import RealRooted.Graph.IndependencePolynomial.ClawFree
import RealRooted.Graph.IndependencePolynomial.CliqueDeletion
import RealRooted.Graph.IndependencePolynomial.CliqueDeletionCompatibility
import RealRooted.Graph.IndependencePolynomial.Multivariate
import RealRooted.Graph.IndependencePolynomial.Recurrence
import RealRooted.Graph.LeakeRyder
import RealRooted.Graph.MatchingPolynomial
import RealRooted.Graph.MatchingPolynomial.Multivariate
import RealRooted.Graph.MinimaPolynomial
import RealRooted.GraceHalfPlane
import RealRooted.GustafssonSolus
import RealRooted.Hadamard
import RealRooted.Hadamard.Basic
import RealRooted.Hadamard.Finite
import RealRooted.Hadamard.Newton
import RealRooted.Hadamard.Cubic
import RealRooted.Hadamard.Grace
import RealRooted.Hadamard.GarloffWagner
import RealRooted.Hadamard.Hurwitz
import RealRooted.Hadamard.Consequences
import RealRooted.HadamardProduct
import RealRooted.HeilmannLieb
import RealRooted.Hermite
import RealRooted.Hermite.Basic
import RealRooted.Hermite.Favard
import RealRooted.Hermite.Orthogonality
import RealRooted.Hermite.Orthogonality.Integral
import RealRooted.Hermite.Roots
import RealRooted.HermiteBiehler
import RealRooted.HermiteBiehler.Basic
import RealRooted.HermiteBiehler.Converse
import RealRooted.HermiteBiehler.Converse.RootGeometry
import RealRooted.HermiteBiehler.Converse.Wronskian
import RealRooted.HermiteBiehler.ConverseLowDegree
import RealRooted.HermiteBiehler.Forward
import RealRooted.HermiteBiehler.Hurwitz
import RealRooted.HermiteBiehler.LogDerivative
import RealRooted.HermiteBiehler.OddEven
import RealRooted.HermitePoulain
import RealRooted.HomogeneousComponentStability
import RealRooted.HomogeneousOre
import RealRooted.HomogeneousOreExamples
import RealRooted.HomogeneousStability
import RealRooted.Hyperbolicity
import RealRooted.HosterStumpInterlacing
import RealRooted.HurwitzMatrix
import RealRooted.InterlacingClosure
import RealRooted.InterlacingConeBounds
import RealRooted.InterlacingSequence
import RealRooted.InterlacingSequenceBasic
import RealRooted.InterlacingSequence.NonnegativeShift
import RealRooted.Interlacing.Multiplicity
import RealRooted.Interlacing.NegativeRoots
import RealRooted.Interlacing.Residue
import RealRooted.IteratedDerivativeShift
import RealRooted.Jacobi
import RealRooted.Jacobi.DifferentialOperator
import RealRooted.Jacobi.Favard
import RealRooted.Jacobi.Orthogonality
import RealRooted.Jacobi.Orthogonality.Integral
import RealRooted.JacobiBetaZeroOrthogonality
import RealRooted.JacobiMarkoff
import RealRooted.JacobiOrthogonality
import RealRooted.JacobiParameterInterlacing
import RealRooted.JensenPencilContraction
import RealRooted.JensenPencilPositiveContraction
import RealRooted.Kurtz
import RealRooted.Laguerre
import RealRooted.Laguerre.Favard
import RealRooted.Laguerre.Orthogonality
import RealRooted.Laguerre.Orthogonality.Integral
import RealRooted.Laguerre.Roots
import RealRooted.Legendre
import RealRooted.Legendre.Basic
import RealRooted.Legendre.Roots
import RealRooted.LiebSokal
import RealRooted.LiebSokalBoundary
import RealRooted.LiebSokalOperator
import RealRooted.LiebSokalOperator.Linearity
import RealRooted.LiebSokalPointwise
import RealRooted.Linear
import RealRooted.LinearPowerFamily
import RealRooted.LiuOppositeSigns
import RealRooted.LiuOppositeSigns.BoundedIntervalContinuity
import RealRooted.LiuOppositeSigns.CommonInterleaverConsequences
import RealRooted.LiuOppositeSigns.Corollary22
import RealRooted.LiuOppositeSigns.DeletionBranches
import RealRooted.LiuOppositeSigns.DerivativeShiftRegularization
import RealRooted.LiuOppositeSigns.DerivativeShiftSequenceRegularization
import RealRooted.LiuOppositeSigns.FactorReturnAssembly
import RealRooted.LiuOppositeSigns.FactorReturnAssembly.DegreeCaseAssembly
import RealRooted.LiuOppositeSigns.FactorReturnAssembly.LeftDegreeCases
import RealRooted.LiuOppositeSigns.FactorReturnAssembly.PredicateDegreeCases
import RealRooted.LiuOppositeSigns.FactorReturnAssembly.RightDegreeCases
import RealRooted.LiuOppositeSigns.FactorReturnLeft
import RealRooted.LiuOppositeSigns.FactorReturnStatements
import RealRooted.LiuOppositeSigns.FactorReturnTwoDegree
import RealRooted.LiuOppositeSigns.ForwardCubicLinear
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.Average
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.LowerSideDouble
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.LowerSideStrict
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.MiddleGap
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RightProtruding
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderAssembly
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderLower
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderMiddle
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderStatement
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderUpper
import RealRooted.LiuOppositeSigns.ForwardLowDegree
import RealRooted.LiuOppositeSigns.JensenRootCount
import RealRooted.LiuOppositeSigns.NoCommonRoots
import RealRooted.LiuOppositeSigns.NonnegCoeffs
import RealRooted.LiuOppositeSigns.PositiveSplitPair
import RealRooted.LiuOppositeSigns.PositiveSplitRootCount
import RealRooted.LiuOppositeSigns.RootCount
import RealRooted.LiuOppositeSigns.RootCountClosure
import RealRooted.LiuOppositeSigns.RootCountRelStability
import RealRooted.LiuOppositeSigns.RootDeletion
import RealRooted.LiuOppositeSigns.Theorem21Assembly
import RealRooted.LiuOppositeSigns.Theorem21Statements
import RealRooted.LiuOppositeSigns.Theorem21Statements.CommonRootDeletion
import RealRooted.LiuOppositeSigns.Theorem21Statements.Interfaces
import RealRooted.LiuOppositeSigns.Theorem21Statements.NoCommonCrossing
import RealRooted.LiuOppositeSigns.Theorem21Statements.NoCommonCrossing.BranchConsequences
import RealRooted.LiuOppositeSigns.Theorem21Statements.NoCommonCrossing.CrossOwnedGaps
import RealRooted.LiuOppositeSigns.Theorem21Statements.NoCommonCrossing.Witnesses
import RealRooted.LiuOppositeSigns.XSub.CubicCubic
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.Basic
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.CubicSubQuadratic
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.Endpoints
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.LeftOutlier
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.LeftRepeated
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.MiddleCases
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.RightRepeated
import RealRooted.LiuOppositeSigns.XSub.CubicQuadratic
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.GapCounts
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.LeftSuccessor
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.RightSuccessor
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.RootFilters
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.SameDegree
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.SplitEndpoints
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.TailSigns
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.UpperTail
import RealRooted.LiuOppositeSigns.XSub.ProperPosition
import RealRooted.LiuOppositeSigns.XSub.LeftSucc
import RealRooted.LiuOppositeSigns.XSub.LeftSuccDegreeThree
import RealRooted.LiuOppositeSigns.XSub.LeftSuccDegreeTwo
import RealRooted.LiuOppositeSigns.XSub.LinearQuadratic
import RealRooted.LiuOppositeSigns.XSub.QuadraticCubic
import RealRooted.LiuOppositeSigns.XSub.QuadraticQuadratic
import RealRooted.LiuOppositeSigns.XSub.QuarticCubic
import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary
import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary.Assembly
import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary.EndpointZero
import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary.QuarticSubQuadratic
import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary.RepeatedLeft
import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary.RepeatedRight
import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary.Statements
import RealRooted.LiuOppositeSigns.XSub.QuarticCubicCommonRoot
import RealRooted.LiuOppositeSigns.XSub.SameDegree
import RealRooted.LiuOppositeSigns.XSub.SplittingTools
import RealRooted.LiuOppositeSignsTheorem
import RealRooted.LiuWang
import RealRooted.LiuWang.OneAddXPositive
import RealRooted.LiuWang.SequenceCore
import RealRooted.LiuWang.SequenceIntervals
import RealRooted.LiuWang.SequencePositive
import RealRooted.LiuWang.SequenceProducts
import RealRooted.LiuWang.Step
import RealRooted.LiuWangBenchmark
import RealRooted.LiuWangRecursion
import RealRooted.LowerTriangularMatrix
import RealRooted.MaWang
import RealRooted.MaWang.CountBounds
import RealRooted.MaWang.Derivative
import RealRooted.MaWang.DerivativeCore
import RealRooted.MaWang.DerivativeDenominator
import RealRooted.MaWang.DerivativeSequence
import RealRooted.MaWang.DerivativeStep
import RealRooted.MaWang.StrictSigns
import RealRooted.MaWang.StrictSigns.Assembly
import RealRooted.MaWang.StrictSigns.RootSigns
import RealRooted.MaWang.StrictStep
import RealRooted.MaWang.Strong
import RealRooted.MaWang.Weak
import RealRooted.MaWang.Weak.Endpoint
import RealRooted.MaWang.Weak.Regularization
import RealRooted.MaWang.Weak.SameDegree
import RealRooted.MaWang.Weak.Successor
import RealRooted.MagnitudeDominated
import RealRooted.MaoWangMatrixProduct
import RealRooted.Mathlib.Algebra.MvPolynomial.Degrees
import RealRooted.Mathlib.Algebra.MvPolynomial.Equiv
import RealRooted.Mathlib.Algebra.MvPolynomial.EvalOnVars
import RealRooted.Mathlib.Algebra.MvPolynomial.Homogenize
import RealRooted.Mathlib.Algebra.MvPolynomial.Nonnegative
import RealRooted.Mathlib.Algebra.MvPolynomial.PDeriv
import RealRooted.Mathlib.Algebra.MvPolynomial.Specialize
import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.DegreeBox
import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.Symbol
import RealRooted.Mathlib.Algebra.Order.BigOperators.Alternating
import RealRooted.Mathlib.Algebra.Order.BigOperators.Ring.Multiset
import RealRooted.Mathlib.Algebra.LinearRecurrence.Annihilator
import RealRooted.Mathlib.Algebra.LinearRecurrence.Quadratic
import RealRooted.Mathlib.Algebra.LinearRecurrence.Quadratic.Chebyshev
import RealRooted.Mathlib.Algebra.LinearRecurrence.Quadratic.Chebyshev.Trigonometric
import RealRooted.Mathlib.Algebra.LinearRecurrence.Quadratic.Factors
import RealRooted.Mathlib.Algebra.LinearRecurrence.Quadratic.Norm
import RealRooted.Mathlib.Algebra.LinearRecurrence.Quadratic.Norm.Real
import RealRooted.Mathlib.Algebra.LinearRecurrence.Quadratic.Rescale
import RealRooted.Mathlib.Algebra.LinearRecurrence.Quadratic.Rescale.Real
import RealRooted.Applications.OEIS.A272471.Recurrence
import RealRooted.Mathlib.Algebra.Polynomial.Basic
import RealRooted.Mathlib.Algebra.Polynomial.Coeff
import RealRooted.Mathlib.Algebra.Polynomial.BasisTransform
import RealRooted.Mathlib.Algebra.Polynomial.Bezoutian
import RealRooted.Mathlib.Algebra.Polynomial.CayleyTransform
import RealRooted.Mathlib.Algebra.Polynomial.CayleyTransform.Algebra
import RealRooted.Mathlib.Algebra.Polynomial.CayleyTransform.Basic
import RealRooted.Mathlib.Algebra.Polynomial.CayleyTransform.Roots
import RealRooted.Mathlib.Algebra.Polynomial.Chow
import RealRooted.Mathlib.Algebra.Polynomial.Degree.Operations
import RealRooted.Mathlib.Algebra.Polynomial.Degree.SmallDegree
import RealRooted.Mathlib.Algebra.Polynomial.Derivative
import RealRooted.Mathlib.Algebra.Polynomial.DifferentialEquation.SecondOrder
import RealRooted.Mathlib.Algebra.Polynomial.Dominance
import RealRooted.Mathlib.Algebra.Polynomial.Expand.Splits
import RealRooted.Mathlib.Algebra.LinearRecurrence.Quadratic.Scale
import RealRooted.Mathlib.Algebra.Polynomial.Eval.Defs
import RealRooted.Mathlib.Algebra.Polynomial.Eval.Degree
import RealRooted.Mathlib.Algebra.Polynomial.Eval.ShiftedChoose
import RealRooted.Mathlib.Algebra.Group.ForwardDiff
import RealRooted.Mathlib.Algebra.Polynomial.Homogenize
import RealRooted.Mathlib.Algebra.Polynomial.Moment
import RealRooted.Mathlib.Algebra.Polynomial.Reverse
import RealRooted.Mathlib.Algebra.Polynomial.Roots
import RealRooted.Mathlib.Algebra.Polynomial.Splits
import RealRooted.Mathlib.Algebra.Polynomial.Splits.Complex
import RealRooted.Mathlib.Algebra.Polynomial.Splits.Derivative
import RealRooted.Mathlib.Analysis.Complex.OpenMapping
import RealRooted.Mathlib.Analysis.Complex.Polynomial.ClosedRoots
import RealRooted.Mathlib.Analysis.Complex.Polynomial.ClosedRoots.Real
import RealRooted.Mathlib.Analysis.Normed.Field.Approximation
import RealRooted.Mathlib.Analysis.Polynomial.Asymptotics
import RealRooted.Mathlib.Analysis.Polynomial.MahlerMeasure
import RealRooted.Mathlib.RingTheory.PowerSeries.CatalanQuadratic
import RealRooted.Mathlib.RingTheory.PowerSeries.CausalFwdDiff
import RealRooted.Mathlib.Topology.Algebra.InfiniteSum.Int
import RealRooted.Mathlib.Topology.Algebra.Polynomial
import RealRooted.Mathlib.Topology.Instances.Matrix.Determinant
import RealRooted.Mathlib.Analysis.SpecialFunctions.ExpIntegral
import RealRooted.Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
import RealRooted.Mathlib.Analysis.SpecialFunctions.Gamma.Beta
import RealRooted.Mathlib.Analysis.SpecialFunctions.Choose
import RealRooted.Mathlib.Analysis.Normed.Ring.Power
import RealRooted.Mathlib.Analysis.SpecialFunctions.Integrals.RpowLog
import RealRooted.Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import RealRooted.Mathlib.Combinatorics.Enumerative.OrderedSubsetPairs
import RealRooted.Mathlib.Data.Fin.Basic
import RealRooted.Mathlib.Order.Fin.Tuple
import RealRooted.Mathlib.Data.List.Basic
import RealRooted.Mathlib.Data.List.Destutter
import RealRooted.Mathlib.Data.List.Interleave
import RealRooted.Mathlib.Data.List.Interleave.Padding
import RealRooted.Mathlib.Data.List.OfFn
import RealRooted.Mathlib.Data.List.Sort.Endpoint
import RealRooted.Mathlib.Data.List.SplitBy
import RealRooted.Mathlib.Data.List.Zip
import RealRooted.Mathlib.Data.Multiset.Card
import RealRooted.Mathlib.Data.Multiset.Rel
import RealRooted.Mathlib.Data.Nat.Cast.Basic
import RealRooted.Mathlib.Data.Nat.Choose.Cast
import RealRooted.Mathlib.Data.Nat.Choose.Nanjundiah
import RealRooted.Mathlib.LinearAlgebra.Matrix.Compound
import RealRooted.Mathlib.LinearAlgebra.Matrix.CompoundSpectrum
import RealRooted.Mathlib.LinearAlgebra.Matrix.Charpoly.Rank
import RealRooted.Mathlib.LinearAlgebra.Matrix.Charpoly.Submatrix
import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.BandedHessenberg
import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.CauchyBinet
import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.ColumnDifference
import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Integral
import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Plucker
import RealRooted.Mathlib.LinearAlgebra.Matrix.GantmacherKrein
import RealRooted.Mathlib.LinearAlgebra.Matrix.Gaussian
import RealRooted.Mathlib.LinearAlgebra.Matrix.Hurwitz
import RealRooted.Mathlib.LinearAlgebra.Matrix.Hurwitz.Determinant
import RealRooted.Mathlib.LinearAlgebra.Matrix.KernelSignVariation
import RealRooted.Mathlib.LinearAlgebra.Matrix.Oscillatory
import RealRooted.Mathlib.LinearAlgebra.Matrix.OscillatoryInterlacing
import RealRooted.Mathlib.LinearAlgebra.Matrix.OscillatoryInterlacing.Core
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Auxiliary
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.CStarClasses
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.CollatzWielandt
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.DataList
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Dominance
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.ExtremeValueUSC
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Irreducible
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Lemmas
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Nonneg
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Primitive
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.QuiverPath
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Spectrum
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Uniqueness
import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegular
import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularRankDeficient
import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularStrictification
import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularVariation
import RealRooted.Mathlib.LinearAlgebra.Matrix.SignVariation
import RealRooted.Mathlib.LinearAlgebra.Matrix.SignVariationTopology
import RealRooted.Mathlib.LinearAlgebra.Matrix.SpectrumClosed
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.Cryer
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.Bidiagonal
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.Charpoly
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.Closure
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.CornerPerturbation
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.Density
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.FinTruncation
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.Mul
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.PrincipalInterlacing
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.Spectrum
import RealRooted.Mathlib.LinearAlgebra.Matrix.Triangularize
import RealRooted.Mathlib.LinearAlgebra.Matrix.VariationDiminishing
import RealRooted.Mathlib.LinearAlgebra.Vandermonde
import RealRooted.Mathlib.RingTheory.MvPolynomial.EulerIdentity
import RealRooted.Mathlib.RingTheory.MvPolynomial.Homogeneous
import RealRooted.Mathlib.RingTheory.MvPolynomial.Hyperbolic
import RealRooted.Mathlib.RingTheory.MvPolynomial.Symmetric
import RealRooted.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
import RealRooted.Mathlib.RingTheory.Polynomial.Jacobi
import RealRooted.Mathlib.RingTheory.Polynomial.Jacobi.DifferentialOperator
import RealRooted.Mathlib.RingTheory.Polynomial.Jacobi.Moment
import RealRooted.Mathlib.RingTheory.Polynomial.Hermite
import RealRooted.Mathlib.RingTheory.Polynomial.Laguerre
import RealRooted.Mathlib.RingTheory.Polynomial.Laguerre.Basic
import RealRooted.Mathlib.RingTheory.Polynomial.Laguerre.Differential
import RealRooted.Mathlib.RingTheory.Polynomial.Laguerre.Recurrence
import RealRooted.Mathlib.RingTheory.Polynomial.Pochhammer
import RealRooted.Mathlib.RingTheory.Polynomial.ShiftedLegendre
import RealRooted.Mathlib.RingTheory.Polynomial.Vieta
import RealRooted.Mathlib.RingTheory.Polynomial.Wronskian
import RealRooted.MatrixInterlacing
import RealRooted.MatrixInterlacing.Action
import RealRooted.MatrixInterlacing.AffinePair
import RealRooted.MatrixInterlacing.Converse
import RealRooted.MatrixInterlacing.Preservation
import RealRooted.MatrixInterlacing.PrincipalInterlacingExamples
import RealRooted.MatrixInterlacing.SparseTests
import RealRooted.MatrixInterlacing.TotallyNonnegative
import RealRooted.MatrixInterlacing.TotallyNonnegativeExamples
import RealRooted.MatrixInterlacingClosure
import RealRooted.Multiaffine
import RealRooted.MultiaffineReciprocal
import RealRooted.MultiaffineReciprocalRight
import RealRooted.MultiplierSequence
import RealRooted.MultiplierSequence.Bidiagonal
import RealRooted.MultiplierSequence.Bidiagonal.Jensen
import RealRooted.MultiplierSequence.Bidiagonal.Jensen.Contraction
import RealRooted.MultiplierSequence.Bidiagonal.Jensen.CubicResidual
import RealRooted.MultiplierSequence.Bidiagonal.Jensen.CubicResidual.Quadratic
import RealRooted.MultiplierSequence.Bidiagonal.Jensen.LowDegree
import RealRooted.MultiplierSequence.Bidiagonal.SecondDerivative
import RealRooted.MultiplierSequence.Infinite
import RealRooted.MultiplierSequence.Sign
import RealRooted.MultiplierSequence.PolyaSchur
import RealRooted.MultiplierSequence.PolyaSchur.Analytic
import RealRooted.MultiplierSequence.PolyaSchur.Factorial
import RealRooted.MultiplierSequence.PolyaSchur.Growth
import RealRooted.MultiplierSequence.PolyaSchur.LaguerrePolya
import RealRooted.MultiplierSequence.PolyaSchur.LaguerrePolya.Derivative
import RealRooted.MultiplierSequence.PolyaSchur.LaguerrePolya.TypeI
import RealRooted.MultiplierSequence.PolyaSchur.LaguerrePolya.TypeIReverse
import RealRooted.MultiplierSequence.PolyaSchur.LaguerrePolya.TypeISigned
import RealRooted.MultiplierSequence.PolyaSchur.LaguerrePolya.Zeros
import RealRooted.MultiplierSequence.PolyaSchur.LaguerrePolya.Examples
import RealRooted.MultiplierSequence.PolyaSchur.Limit
import RealRooted.MultivariateHeilmannLieb
import RealRooted.MultivariateStability
import RealRooted.NarayanaTransformation
import RealRooted.NarayanaTransformation.Basis
import RealRooted.NarayanaTransformation.Basis.Stirling
import RealRooted.NarayanaTransformation.Coefficients
import RealRooted.NarayanaTransformation.Composition
import RealRooted.NarayanaTransformation.Endpoints
import RealRooted.NarayanaTransformation.Falling
import RealRooted.NarayanaTransformation.Gamma
import RealRooted.NarayanaTransformation.Rectangular
import RealRooted.NarayanaTransformation.Rectangular.LowDegree
import RealRooted.NarayanaTransformation.Rectangular.Narayana
import RealRooted.NarayanaTransformation.Rectangular.Preservation
import RealRooted.NarayanaTransformation.Recurrences
import RealRooted.NarayanaTransformation.Recurrences.Identities
import RealRooted.NarayanaTransformation.Recurrences.Interlacing
import RealRooted.NarayanaTransformation.Rising
import RealRooted.NarayanaTransformation.RootGeometry
import RealRooted.NarayanaTransformation.SimpleRoots
import RealRooted.NewtonAux
import RealRooted.OEIS.A046802
import RealRooted.ObreschkoffContinuity
import RealRooted.ObreschkoffConverse
import RealRooted.ObreschkoffConverse.Converse
import RealRooted.ObreschkoffConverse.DegreeGap
import RealRooted.ObreschkoffConverse.Derivative
import RealRooted.ObreschkoffConverse.Forward
import RealRooted.ObreschkoffConverse.Regularization
import RealRooted.OscillatoryInterlacing
import RealRooted.OperatorPreservesInterlacing
import RealRooted.OrderedRoots
import RealRooted.ParkingFunctions.Descents.Basic
import RealRooted.ParkingFunctions.Descents.ChainSort
import RealRooted.ParkingFunctions.Descents.DescentChains
import RealRooted.ParkingFunctions.Descents.DiaconisHicks
import RealRooted.ParkingFunctions.Descents.Literal
import RealRooted.ParkingFunctions.Descents.LiteralRecurrence
import RealRooted.ParkingFunctions.Descents.Words
import RealRooted.ParkingFunctions.ToricContribution.CommonInterlacer
import RealRooted.ParkingFunctions.ToricContribution.ContributionReversal
import RealRooted.ParkingFunctions.ToricContribution.Definitions
import RealRooted.ParkingFunctions.ToricContribution.DiagonalCollapse
import RealRooted.ParkingFunctions.ToricContribution.ExceptionalOffset
import RealRooted.ParkingFunctions.ToricContribution.ExceptionalOffset.BaseAndMoments
import RealRooted.ParkingFunctions.ToricContribution.ExceptionalOffset.NodeInterlacing
import RealRooted.ParkingFunctions.ToricContribution.ExceptionalOffset.PencilSplitting
import RealRooted.ParkingFunctions.ToricContribution.ExceptionalOffset.ProperPositionAndParameters
import RealRooted.ParkingFunctions.ToricContribution.FiniteOffsets
import RealRooted.ParkingFunctions.ToricContribution.IntervalInsertion
import RealRooted.ParkingFunctions.ToricContribution.TriangleInvariant
import RealRooted.ParkingFunctions.ToricContribution.TriangleAlgebra
import RealRooted.PFPolynomial
import RealRooted.PFPolynomial.LinearFactor
import RealRooted.PartialSumStep
import RealRooted.PartialSymmetrization
import RealRooted.Polarization
import RealRooted.PolyaFrequency.EventuallyPolynomial
import RealRooted.PolyaFrequencyConvolution
import RealRooted.PolyaFrequencyConvolution.Basic
import RealRooted.PolyaFrequencyConvolution.InverseOneSubPow
import RealRooted.PolynomialValueEulerNumerator
import RealRooted.PolynomialValueEulerNumerator.PF
import RealRooted.PolynomialValueEulerNumerator.Product
import RealRooted.PolynomialValueEulerNumerator.Product.PF
import RealRooted.PosCombo
import RealRooted.PosCombo.Degree
import RealRooted.PositiveParameterLocalLowerCount
import RealRooted.ProductFamily
import RealRooted.ProductOrientation
import RealRooted.ProductSequence
import RealRooted.ProductSequence.Core
import RealRooted.ProductSequence.EndpointPair
import RealRooted.ProductSequence.FactorFamilies
import RealRooted.ProductSequence.Factors
import RealRooted.ProductSequence.Lifts
import RealRooted.ProductSequence.ScalarFamilies
import RealRooted.QuadraticCubicPencil
import RealRooted.QuadraticRoot
import RealRooted.RankTwoMatching
import RealRooted.RankTwoMatching.Basic
import RealRooted.RankTwoMatching.DisjointEquiv
import RealRooted.RankTwoMatching.Endpoint
import RealRooted.RankTwoMatching.Enumeration
import RealRooted.RankTwoMatching.Orientation
import RealRooted.RankTwoMatching.Transform
import RealRooted.RankTwoMatchingModel
import RealRooted.RectangularConvolution
import RealRooted.RectangularConvolutionIdentity
import RealRooted.RectangularPolarization
import RealRooted.RectangularPolarizationComplement
import RealRooted.RecurrenceDiscriminant
import RealRooted.ReflectedRootCountLocalConstancy
import RealRooted.ReciprocalShift.Interlacing
import RealRooted.ReciprocalShift.Interlacing.Inversion
import RealRooted.ReciprocalShift.ProperPosition
import RealRooted.ReciprocalShift.Roots
import RealRooted.RootAmplitude
import RealRooted.RootAmplitude.Convex
import RealRooted.RootAmplitude.Density
import RealRooted.RootAmplitude.Extension
import RealRooted.RootAmplitude.Extreme
import RealRooted.RootAmplitude.Finite
import RealRooted.RootAmplitude.Minimum
import RealRooted.RootAmplitude.Polynomial
import RealRooted.RootAmplitude.Separation
import RealRooted.RootAmplitude.Separation.Euler
import RealRooted.RootAmplitude.Separation.Finite
import RealRooted.RootAmplitude.Separation.Polynomial
import RealRooted.RootAmplitude.Separation.Roots
import RealRooted.RootAmplitude.SmallestRoot
import RealRooted.RootAmplitude.SumSquares
import RealRooted.RootBounds
import RealRooted.RootContinuity
import RealRooted.RootCountFinite
import RealRooted.RootCountJump
import RealRooted.RootCountLocalConstancy
import RealRooted.RootCounting
import RealRooted.RootCounting.Finite
import RealRooted.RootCounting.SignChanges
import RealRooted.RootCounting.Threshold
import RealRooted.RootCounting.Threshold.Anchor
import RealRooted.RootCounting.Threshold.Basic
import RealRooted.RootCounting.Threshold.Derivative
import RealRooted.RootCounting.Threshold.DominanceFamily
import RealRooted.RootCounting.Threshold.LogConcavity
import RealRooted.RootCounting.Threshold.Signs
import RealRooted.RootCounting.Threshold.Sorted
import RealRooted.RootMatchingSort
import RealRooted.RootMultiplicityMatching
import RealRooted.RootOrderBridge
import RealRooted.RootSumBounds
import RealRooted.RootVieta
import RealRooted.RootVieta.Newton
import RealRooted.RowThreshold
import RealRooted.RowThresholdOne
import RealRooted.SameDegreeCountFromAnalytic
import RealRooted.SameDegreeCubicRootCount
import RealRooted.SameDegreeCubicSecondRootFromAnalytic
import RealRooted.SameDegreeDerivative
import RealRooted.SameDegreeMultiplicityLowerCount
import RealRooted.SameDegreeQuadraticObstruction
import RealRooted.SameDegreeQuadraticRootCount
import RealRooted.SamePhaseStability
import RealRooted.SamePhaseInterlacing
import RealRooted.ScalarNormalization
import RealRooted.SequenceClosure
import RealRooted.ShiftLemma
import RealRooted.SignEvaluation
import RealRooted.SmallPositiveParameterCount
import RealRooted.SimpleRoots
import RealRooted.SortedRoots
import RealRooted.SortedRoots.Exhibited
import RealRooted.StaircaseSum
import RealRooted.SuccDegreeLeftEndpoint
import RealRooted.SuccDegreeRootCrossing
import RealRooted.SymmetricDecomposition
import RealRooted.SymmetricDecomposition.Decomposition
import RealRooted.SymmetricDecomposition.Definitions
import RealRooted.SymmetricDecomposition.FPolynomial
import RealRooted.SymmetricDecomposition.FPolynomialInterlacing
import RealRooted.SymmetricDecomposition.Theorem26
import RealRooted.Tactic
import RealRooted.Tactic.AffineDerivative
import RealRooted.Tactic.AissenSchoenbergWhitney
import RealRooted.Tactic.AllCombo
import RealRooted.Tactic.Attr
import RealRooted.Tactic.Bezoutian
import RealRooted.Tactic.CoefficientShape
import RealRooted.Tactic.CommonInterleaver
import RealRooted.Tactic.CommonInterleaver.AnalyticRules
import RealRooted.Tactic.CommonInterleaver.AnalyticSyntax
import RealRooted.Tactic.CommonInterleaver.BasicRules
import RealRooted.Tactic.CommonInterleaver.BasicSyntax
import RealRooted.Tactic.CommonInterleaver.Core
import RealRooted.Tactic.CommonInterleaver.FamilyRules
import RealRooted.Tactic.CommonInterleaver.FamilySyntax
import RealRooted.Tactic.CommonInterleaver.LowDegreeRules
import RealRooted.Tactic.CommonInterleaver.LowDegreeSyntax
import RealRooted.Tactic.CubicDiscriminant
import RealRooted.Tactic.Derivative
import RealRooted.Tactic.EndpointDerivative
import RealRooted.Tactic.EulerOperator
import RealRooted.Tactic.Examples
import RealRooted.Tactic.Examples.AffineDerivative
import RealRooted.Tactic.Examples.AissenSchoenbergWhitney
import RealRooted.Tactic.Examples.AllCombo
import RealRooted.Tactic.Examples.Attr
import RealRooted.Tactic.Examples.Bezoutian
import RealRooted.Tactic.Examples.CoefficientShape
import RealRooted.Tactic.Examples.Combinatorial
import RealRooted.Tactic.Examples.CommonInterleaver
import RealRooted.Tactic.Examples.CubicDiscriminant
import RealRooted.Tactic.Examples.Derivative
import RealRooted.Tactic.Examples.EndpointDerivative
import RealRooted.Tactic.Examples.EulerOperator
import RealRooted.Tactic.Examples.Favard
import RealRooted.Tactic.Examples.Finish
import RealRooted.Tactic.Examples.FiniteSymbol
import RealRooted.Tactic.Examples.FiniteSymbolPF
import RealRooted.Tactic.Examples.GammaRealRoots
import RealRooted.Tactic.Examples.GeneralizedLaguerre
import RealRooted.Tactic.Examples.Hadamard
import RealRooted.Tactic.Examples.HermiteBiehler
import RealRooted.Tactic.Examples.HermitePoulain
import RealRooted.Tactic.Examples.HomogenizeStable
import RealRooted.Tactic.Examples.I2DerivativeLag
import RealRooted.Tactic.Examples.InterlacingSequence
import RealRooted.Tactic.Examples.IteratedDerivativeShift
import RealRooted.Tactic.Examples.IteratedDerivativeShiftProduct
import RealRooted.Tactic.Examples.J1Chebyshev
import RealRooted.Tactic.Examples.J1Gap3Reciprocal
import RealRooted.Tactic.Examples.Kurtz
import RealRooted.Tactic.Examples.Linear
import RealRooted.Tactic.Examples.LinearPowerFamily
import RealRooted.Tactic.Examples.LiuWang
import RealRooted.Tactic.Examples.LiuWang.ActiveSteps
import RealRooted.Tactic.Examples.LiuWang.AffineHalfLine
import RealRooted.Tactic.Examples.LiuWang.CurrentFactors
import RealRooted.Tactic.Examples.LiuWang.GenericNonpositive
import RealRooted.Tactic.Examples.LiuWang.InferredCertificates
import RealRooted.Tactic.Examples.LiuWang.InnerWindow
import RealRooted.Tactic.Examples.LiuWang.Interval
import RealRooted.Tactic.Examples.LiuWang.NegativeInnerWindow
import RealRooted.Tactic.Examples.LiuWang.NonpositiveGlobal
import RealRooted.Tactic.Examples.LiuWang.PositiveAffine
import RealRooted.Tactic.Examples.LiuWang.ProductSequences
import RealRooted.Tactic.Examples.LiuWang.QuadraticSequences
import RealRooted.Tactic.Examples.LiuWang.Step
import RealRooted.Tactic.Examples.LiuWang.StrictPositiveLag
import RealRooted.Tactic.Examples.LiuWang.StrictProducts
import RealRooted.Tactic.Examples.LiuWangRecursion
import RealRooted.Tactic.Examples.Lookup
import RealRooted.Tactic.Examples.MaWang
import RealRooted.Tactic.Examples.MaWang.AtomicWindows
import RealRooted.Tactic.Examples.MaWang.DirectSteps
import RealRooted.Tactic.Examples.MaWang.FactorWindows
import RealRooted.Tactic.Examples.MaWang.LiuWang
import RealRooted.Tactic.Examples.MaWang.NonnegativeDenominator
import RealRooted.Tactic.Examples.MaWang.NonposAffineSequences
import RealRooted.Tactic.Examples.MaWang.ScalarWindows
import RealRooted.Tactic.Examples.MaWang.WeakSequences
import RealRooted.Tactic.Examples.MaWang.XFactorSequences
import RealRooted.Tactic.Examples.MagnitudeDominated
import RealRooted.Tactic.Examples.Matrix
import RealRooted.Tactic.Examples.MultiplierSequence
import RealRooted.Tactic.Examples.Narayana
import RealRooted.Tactic.Examples.OEIS
import RealRooted.Tactic.Examples.OEIS.ClassicalFamilies
import RealRooted.Tactic.Examples.OEIS.CompatCommon
import RealRooted.Tactic.Examples.OEIS.DerivativeLag
import RealRooted.Tactic.Examples.OEIS.DifferentialOperators
import RealRooted.Tactic.Examples.OEIS.DifferentialPreservers
import RealRooted.Tactic.Examples.OEIS.Favard
import RealRooted.Tactic.Examples.OEIS.Foundation
import RealRooted.Tactic.Examples.OEIS.GammaVeronese
import RealRooted.Tactic.Examples.OEIS.LinearPower
import RealRooted.Tactic.Examples.OEIS.LowDegreeRootCount
import RealRooted.Tactic.Examples.OEIS.NegativeLag
import RealRooted.Tactic.Examples.OEIS.ParityEndpoint
import RealRooted.Tactic.Examples.OEIS.PolyaFrequency
import RealRooted.Tactic.Examples.OEIS.PositiveCombinations
import RealRooted.Tactic.Examples.OEIS.PositiveLag
import RealRooted.Tactic.Examples.OEIS.ProductLift
import RealRooted.Tactic.Examples.OEIS.ProductRouters
import RealRooted.Tactic.Examples.OEIS.ScalarCoeff
import RealRooted.Tactic.Examples.OEIS.SecondDerivative
import RealRooted.Tactic.Examples.OEISPositiveTLag
import RealRooted.Tactic.Examples.OEISTestbed
import RealRooted.Tactic.Examples.OEISTestbed.Favard
import RealRooted.Tactic.Examples.OEISTestbed.LiuWangMixed
import RealRooted.Tactic.Examples.OEISTestbed.MaWangSequences
import RealRooted.Tactic.Examples.OEISTestbed.MaWangSteps
import RealRooted.Tactic.Examples.OEISTestbed.MixedDenominator
import RealRooted.Tactic.Examples.OEISTestbed.NegativeSquare
import RealRooted.Tactic.Examples.OEISTestbed.PromotedMixed
import RealRooted.Tactic.Examples.OEISTestbedLS4
import RealRooted.Tactic.Examples.OperatorPreservesInterlacing
import RealRooted.Tactic.Examples.PFBidiagonal
import RealRooted.Tactic.Examples.PFPolynomial
import RealRooted.Tactic.Examples.PosCombo
import RealRooted.Tactic.Examples.PreservingOperatorSequence
import RealRooted.Tactic.Examples.Product
import RealRooted.Tactic.Examples.Product.Basic
import RealRooted.Tactic.Examples.Product.EndpointPair
import RealRooted.Tactic.Examples.Product.Families
import RealRooted.Tactic.Examples.Product.Lifts
import RealRooted.Tactic.Examples.ReciprocalShift
import RealRooted.Tactic.Examples.RecurrenceIdentification
import RealRooted.Tactic.Examples.RootBounds
import RealRooted.Tactic.Examples.RootCount
import RealRooted.Tactic.Examples.ScalarDen
import RealRooted.Tactic.Examples.SecondDerivative
import RealRooted.Tactic.Examples.SequenceSurvey
import RealRooted.Tactic.Examples.SideGoals
import RealRooted.Tactic.Examples.Sign
import RealRooted.Tactic.Examples.SignAssembly
import RealRooted.Tactic.Examples.StaircaseSum
import RealRooted.Tactic.Examples.SymmetricDecomposition
import RealRooted.Tactic.Examples.VeroneseSection
import RealRooted.Tactic.Examples.Wagner
import RealRooted.Tactic.Examples.WagnerX
import RealRooted.Tactic.Examples.WeightedSum
import RealRooted.Tactic.Favard
import RealRooted.Tactic.Favard.Basic
import RealRooted.Tactic.Favard.Denominator
import RealRooted.Tactic.Favard.DenominatorSyntax
import RealRooted.Tactic.Favard.Direct
import RealRooted.Tactic.Favard.DirectSyntax
import RealRooted.Tactic.Favard.RowSign
import RealRooted.Tactic.Favard.RowSignSyntax
import RealRooted.Tactic.Finish
import RealRooted.Tactic.FiniteSymbol
import RealRooted.Tactic.FiniteSymbolPF
import RealRooted.Tactic.GammaRealRoots
import RealRooted.Tactic.GeneralizedLaguerre
import RealRooted.Tactic.Hadamard
import RealRooted.Tactic.HermiteBiehler
import RealRooted.Tactic.HermitePoulain
import RealRooted.Tactic.HomogenizeStable
import RealRooted.Tactic.I2DerivativeLag
import RealRooted.Tactic.InterlacingSequence
import RealRooted.Tactic.IteratedDerivativeShift
import RealRooted.Tactic.IteratedDerivativeShiftProduct
import RealRooted.Tactic.J1Chebyshev
import RealRooted.Tactic.J1Gap3Reciprocal
import RealRooted.Tactic.Kurtz
import RealRooted.Tactic.Linear
import RealRooted.Tactic.LinearPowerFamily
import RealRooted.Tactic.LiuWang
import RealRooted.Tactic.LiuWang.SequenceIntervals
import RealRooted.Tactic.LiuWang.SequenceNonpositive
import RealRooted.Tactic.LiuWang.SequencePositive
import RealRooted.Tactic.LiuWang.SequenceProducts
import RealRooted.Tactic.LiuWang.SequenceQuadratic
import RealRooted.Tactic.LiuWang.Step
import RealRooted.Tactic.LiuWangRecursion
import RealRooted.Tactic.Lookup
import RealRooted.Tactic.MaWang
import RealRooted.Tactic.MaWang.Basic
import RealRooted.Tactic.MaWang.Denominator
import RealRooted.Tactic.MaWang.DenominatorSyntax
import RealRooted.Tactic.MaWang.Factors
import RealRooted.Tactic.MaWang.FactorSyntax
import RealRooted.Tactic.MaWang.Sequences
import RealRooted.Tactic.MaWang.SequenceSyntax
import RealRooted.Tactic.MaWang.Steps
import RealRooted.Tactic.MaWang.StepSyntax
import RealRooted.Tactic.MagnitudeDominated
import RealRooted.Tactic.Matrix
import RealRooted.Tactic.MultiplierSequence
import RealRooted.Tactic.Named
import RealRooted.Tactic.Narayana
import RealRooted.Tactic.OEIS
import RealRooted.Tactic.OEIS.Basic
import RealRooted.Tactic.OEIS.DerivativeLag
import RealRooted.Tactic.OEIS.NegativeLag
import RealRooted.Tactic.OEIS.PositiveLag
import RealRooted.Tactic.OEIS.ProductExit
import RealRooted.Tactic.OEIS.ProductFactor
import RealRooted.Tactic.OEIS.ProductLift
import RealRooted.Tactic.OEIS.ProductParity
import RealRooted.Tactic.OperatorPreservesInterlacing
import RealRooted.Tactic.PFBidiagonal
import RealRooted.Tactic.PFPolynomial
import RealRooted.Tactic.PosCombo
import RealRooted.Tactic.PreservingOperatorSequence
import RealRooted.Tactic.Product
import RealRooted.Tactic.Product.Rules
import RealRooted.Tactic.Product.Syntax
import RealRooted.Tactic.Product.Syntax.Basic
import RealRooted.Tactic.Product.Syntax.EndpointPair
import RealRooted.Tactic.Product.Syntax.Families
import RealRooted.Tactic.Product.Syntax.Lifts
import RealRooted.Tactic.ReciprocalShift
import RealRooted.Tactic.RecurrenceEval
import RealRooted.Tactic.RecurrenceIdentification
import RealRooted.Tactic.RootBounds
import RealRooted.Tactic.RootCount
import RealRooted.Tactic.RootCount.CoreRules
import RealRooted.Tactic.RootCount.CoreSyntax
import RealRooted.Tactic.RootCount.LowDegree
import RealRooted.Tactic.RootCount.LowDegreeRules
import RealRooted.Tactic.RootCount.LowDegreeSyntax
import RealRooted.Tactic.RootCount.SequenceCore
import RealRooted.Tactic.ScalarDen
import RealRooted.Tactic.SecondDerivative
import RealRooted.Tactic.SideGoals
import RealRooted.Tactic.Sign
import RealRooted.Tactic.SignAssembly
import RealRooted.Tactic.StaircaseSum
import RealRooted.Tactic.SymmetricDecomposition
import RealRooted.Tactic.Targets
import RealRooted.Tactic.VeroneseSection
import RealRooted.Tactic.Wagner
import RealRooted.Tactic.WagnerX
import RealRooted.UnitIntervalGraph.AcyclicSink
import RealRooted.Tactic.WagnerX.Core
import RealRooted.Tactic.WagnerX.Frontend
import RealRooted.Tactic.WagnerX.Obstructions
import RealRooted.Tactic.WagnerX.PositiveLag
import RealRooted.Tactic.WagnerX.Syntax
import RealRooted.Tactic.WagnerX.TranslatedLag
import RealRooted.Tactic.WeightedSum
import RealRooted.ThresholdMatrix
import RealRooted.ThresholdMatrix.Basic
import RealRooted.ThresholdMatrix.GustafssonSolus
import RealRooted.ThresholdMatrix.HaglundZhang
import RealRooted.TotallyNonnegInterlacing
import RealRooted.Touchard
import RealRooted.Transforms.BrandenE
import RealRooted.Transforms.BrandenE.Basic
import RealRooted.Transforms.BrandenE.BasisImage
import RealRooted.Transforms.BrandenE.Inverse
import RealRooted.Transforms.BrandenE.OrderedBell
import RealRooted.Transforms.BrandenE.ProperPosition
import RealRooted.Transforms.BrandenE.WeightedSum
import RealRooted.Transforms.ReverseHermite
import RealRooted.Transforms.ReverseHermite.Basic
import RealRooted.Transforms.ReverseHermite.Derivative
import RealRooted.Transforms.ReverseHermite.Preservation
import RealRooted.TridiagonalDet
import RealRooted.TridiagonalDet.Recurrence
import RealRooted.UpperDerivativeInterlace
import RealRooted.VeroneseMatrix
import RealRooted.VeroneseSection
import RealRooted.VeroneseSectionPair
import RealRooted.VeroneseSectionPair.HermiteBiehler
import RealRooted.Wagner
import RealRooted.Wagner.NonpositiveRoots
import RealRooted.WagnerLeftSum
import RealRooted.WagnerRightSum
import RealRooted.WagnerRightSum.Sign
import RealRooted.WagnerX
import RealRooted.WagnerX.AffineFactors
import RealRooted.WagnerX.ListInterlacing
import RealRooted.WagnerX.NonnegativeRoots
import RealRooted.WagnerX.ProperPosition
import RealRooted.WangYeh.Affine
import RealRooted.WangYeh.Examples
import RealRooted.WangYeh.PF
import RealRooted.WangYeh.TriangularArray
import RealRooted.WangYeh.TriangularMatrix
import RealRooted.WeightedSum
import RealRooted.Wronskian
import RealRooted.Wronskian.Algebra
import RealRooted.Wronskian.Converse
import RealRooted.Wronskian.Forward
import RealRooted.Wronskian.PolarLaguerre
import RealRooted.Wronskian.Successor
import RealRooted.Wronskian.Successor.Gap
import RealRooted.Wronskian.Successor.Interlacing
import RealRooted.Wronskian.Successor.Signs
import RealRooted.Wronskian.Successor.Splits
import RealRooted.GammaPencil.Basic
import RealRooted.GammaPencil.Invariants
import RealRooted.GammaPencil.Preserver
import RealRooted.GammaPencil.Symbol
import RealRooted.GammaPencil.SymbolStability
import RealRooted.GammaPencil.Theorem
import RealRooted.Production
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.Cryer.Strict
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.Cryer.Closure
import RealRooted.PolyaFrequency.EventuallyPolynomial.CausalClosure
import RealRooted.PolyaFrequency.EventuallyPolynomial.CausalClosure.ZeroPrefix
import RealRooted.PolynomialValueEulerNumerator.PF.Causal
import RealRooted.PolynomialValueEulerNumerator.Product.PF.Causal