∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g : ι → β}, Antivary f g → ∀ (n : ℕ), Antivary f (g ^ n)