Model-independent prime-refinement iteration

The shared iteration and partition assembly live in Iteration. This module retains the model-independent public implication interface used by the obstruction proof.

theorem NRR.avvakumov_akopyan_karasev_flexible (H : FlexiblePrimeRefinementTheorem) (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) : 0 < n → ∃ (P : ConvexPartition K n), P.IsFair

Public implication form of the Avvakumov--Akopyan--Karasev theorem. The conclusion for every positive number of pieces follows formally from the single prime-refinement separator theorem.