simple power lemma

Stream: new members

[Matthew Honnor]

Dear all, I was expecting simp to close the following simple lemma but it will not. I have then tried using cardinal.power_add and library search but these didn't work as well. Any help would be great.

import analysis.complex.basic

lemma equality_of_powers { u : ℂ }{ z : ℂ }{k : ℕ }{ b : ℕ }
  ( h : ¬(b < k) ) :
  (z - u) ^ (b - k) * (z - u) ^ k = (z - u) ^ b :=
  begin
    rw ← cardinal.power_add,
  end

Thanks in advance.

[Yaël Dillies]

docs#pow_sub will lead you there

[Yaël Dillies]

Oof. I wrote this message 50min ago