R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n) → IsRightRegular a
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n) ↔ IsRightRegular a
refine' ⟨_, IsRightRegular.pow n⟩
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ Nat.pred n) → IsRightRegular a
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n) → IsRightRegular a
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ]
no goals
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ Nat.pred n) → IsRightRegular a
exact IsRightRegular.of_mul