∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 ≤ f₁ i) → (∀ i ∈ s, 0 < f₂ i) → AntivaryOn f₁ g s → MonovaryOn f₂ g s → AntivaryOn (f₁ / f₂) g s