α : Type ?u.46449
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
x y : M
hxy : x ∣ y
n : ℕ
x✝ : n + 1 ≠ 0
⊢ x ∣ y * y ^ n
α : Type ?u.46449
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
x y : M
hxy : x ∣ y
n : ℕ
x✝ : n + 1 ≠ 0
⊢ x ∣ y ^ (n + 1)
rw [pow_succ]
no goals
α : Type ?u.46449
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
x y : M
hxy : x ∣ y
n : ℕ
x✝ : n + 1 ≠ 0
⊢ x ∣ y * y ^ n
exact hxy.mul_right _