∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i →
    ∃ n, MeasureTheory.SignedMeasure.ExistsOneDivLT✝ s i n