import LeanCanny.Abstract
import LeanCanny.ETR.CoercivePSPACE

/-! # The completed real-algebraic polynomial-space upper bounds

This default entry point exports the ETR and connectivity formal abstract,
including the coercive ETR proof and the native connectivity decisions.
The additional tube, projection, and elimination constructions are available
through `LeanCanny.Alternatives`, built by the `LeanCannyAlternatives` target.
-/