case refine'_1
α : Type u_1
β : Type ?u.356184
γ : Type ?u.356187
δ : Type ?u.356190
inst✝ : CancelCommMonoidWithZero α
q : α
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ ¬IsUnit (q ^ (m - n))

case refine'_2
α : Type u_1
β : Type ?u.356184
γ : Type ?u.356187
δ : Type ?u.356190
inst✝ : CancelCommMonoidWithZero α
q : α
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)
α : Type u_1
β : Type ?u.356184
γ : Type ?u.356187
δ : Type ?u.356190
inst✝ : CancelCommMonoidWithZero α
q : α
hq : ¬IsUnit q
hq' : q ≠ 0
⊢ Function.Injective fun n => q ^ n
refine' injective_of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), _, _⟩
no goals
case refine'_1
α : Type u_1
β : Type ?u.356184
γ : Type ?u.356187
δ : Type ?u.356190
inst✝ : CancelCommMonoidWithZero α
q : α
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ ¬IsUnit (q ^ (m - n))
exact not_isUnit_of_not_isUnit_dvd hq (dvd_pow (dvd_refl _) (Nat.sub_pos_of_lt h).ne')
no goals
case refine'_2
α : Type u_1
β : Type ?u.356184
γ : Type ?u.356187
δ : Type ?u.356190
inst✝ : CancelCommMonoidWithZero α
q : α
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)
exact (pow_mul_pow_sub q h.le).symm