powers of x<1

Stream: maths

[Filippo A. E. Nuccio]

We have that in a normed field K the power function with basis bigger than 1 is (strictly) monotone, but I think we don't have

lemma zpow_strict_anti {K : Type} [linear_ordered_field K] {x : K} (hx₀ : 0 < x) (hx₁ : x < 1) :
  strict_anti (λ n:ℤ, x ^ n) :=
begin
  intros n m H,
  rw [← inv_inv₀ x],
  simp only [inv_zpow₀ x⁻¹, inv_lt_inv (zpow_pos_of_pos (inv_pos.mpr hx₀) _)
    (zpow_pos_of_pos (inv_pos.mpr hx₀) _)],
  exact zpow_strict_mono (one_lt_inv hx₀ hx₁) H,
end

Unless my proof is really horrible, zpow_strict_anti does not seem to me to be an immediate consequence of zpow_strict_mono. In general, many results in docs#integer-power-operation-on-fields-and-division-rings only treat the case x>1; so I was thinking about a general tool containing the first three lines of my proof above, automatically converting all these results into the corresponding one for 0<x<1. Is it a good idea?

[Yury G. Kudryashov]

See docs#zpow_strict_anti

[Yury G. Kudryashov]

I added it in #10895

[Filippo A. E. Nuccio]

Thanks