Factoring at a support class in a tail quotient

After regrouping along a common tail, a class met by the support determines a nonzero convex restriction. Factoring off that restriction leaves an integral cofactor whose nonzero support classes have strictly smaller order type.

theorem HahnSeries.CardSuppLTTruncationIntegerPart.exists_factor_with_smaller_support_class_orderType {G : Type u} {R : Type v} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Module ℚ G] [PosSMulMono ℚ G] [Field R] {κ : Cardinal.{u}} [Fact (Cardinal.aleph0 < κ)] (Z : Subring R) (T : Set (FiniteArchimedeanClass G)) (q : FiniteArchimedeanClass (FiniteArchimedeanClass.TailQuotient T)) (b : ↥(cardSuppLTTruncationIntegerPart Z)) (hqocc : ↑q ∈ ArchimedeanClass.mk '' Submodule.Quotient.mk '' (↑↑b).support) (hne : (filter fun (x : G) => x ∈ AddSubgroup.comap (FiniteArchimedeanClass.tailSubmodule ℚ T).mkQ.toAddMonoidHom q.closedBallAddSubgroup) ↑↑b ≠ 0) : ∃ (t : ↥(cardSuppLTTruncationIntegerPart Z)) (w : ↥(cardSuppLTTruncationIntegerPart Z)), ↑↑t = (filter fun (x : G) => x ∈ AddSubgroup.comap (FiniteArchimedeanClass.tailSubmodule ℚ T).mkQ.toAddMonoidHom q.closedBallAddSubgroup) ↑↑b ∧ b = t * w ∧ ⋯.orderType < ⋯.orderType

Factoring at a tail-quotient class met by the support strictly lowers the order type of the nonzero support classes of the complementary factor.