Bennett cancel power denominator

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.Degree.Operations
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.Tactic.Ring

section
namespace D1Bound5

variable {F : Type*} [Field F] [CharZero F]


theorem _root_.D1Bound5.bennett_cancel_power_denominator (x : F) (hx : x ≠ 0)
    (u v t : ℕ) (h : u = v + t) : x ^ u * (x⁻¹) ^ v = x ^ t := by sorry











end D1Bound5
end