β : Type ?u.278866
A : Type ?u.278869
G : Type ?u.278872
M : Type u_1
R : Type ?u.278878
inst✝ : LinearOrderedCommGroupWithZero M
a : M
m n : ℕ
ha : 1 < a
⊢ 1 * a ^ n < a * a ^ n
β : Type ?u.278866
A : Type ?u.278869
G : Type ?u.278872
M : Type u_1
R : Type ?u.278878
inst✝ : LinearOrderedCommGroupWithZero M
a : M
m n : ℕ
ha : 1 < a
⊢ a ^ n < a ^ Nat.succ n
rw [← one_mul (a ^ n), pow_succ]
no goals
β : Type ?u.278866
A : Type ?u.278869
G : Type ?u.278872
M : Type u_1
R : Type ?u.278878
inst✝ : LinearOrderedCommGroupWithZero M
a : M
m n : ℕ
ha : 1 < a
⊢ 1 * a ^ n < a * a ^ n
exact mul_lt_right₀ _ ha (pow_ne_zero _ (zero_lt_one.trans ha).ne')