∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {f₁ f₂ : ι → α} {g : ι → β},
  0 ≤ f₁ → StrongLT 0 f₂ → Antivary f₁ g → Monovary f₂ g → Antivary (f₁ / f₂) g