∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g : ι → β}, 0 ≤ g → Monovary f g → ∀ (n : ℕ), Monovary f (g ^ n)