case intro
β : Type ?u.39271
A : Type ?u.39274
G : Type ?u.39277
M : Type u_1
R : Type ?u.39283
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : M
n : ℕ
ha : 1 < a
k : ℕ
h : n < Nat.succ n + k
⊢ a ^ n < a ^ (Nat.succ n + k)
β : Type ?u.39271
A : Type ?u.39274
G : Type ?u.39277
M : Type u_1
R : Type ?u.39283
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : M
n m : ℕ
ha : 1 < a
h : n < m
⊢ a ^ n < a ^ m
rcases Nat.le.dest h with ⟨k, rfl⟩
case intro
β : Type ?u.39271
A : Type ?u.39274
G : Type ?u.39277
M : Type u_1
R : Type ?u.39283
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : M
n : ℕ
ha : 1 < a
k : ℕ
⊢ a ^ n < a ^ (Nat.succ n + k)
case intro
β : Type ?u.39271
A : Type ?u.39274
G : Type ?u.39277
M : Type u_1
R : Type ?u.39283
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : M
n : ℕ
ha : 1 < a
k : ℕ
h : n < Nat.succ n + k
⊢ a ^ n < a ^ (Nat.succ n + k)
clear h
case intro
β : Type ?u.39271
A : Type ?u.39274
G : Type ?u.39277
M : Type u_1
R : Type ?u.39283
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : M
n : ℕ
ha : 1 < a
k : ℕ
⊢ a ^ n < a ^ n * a ^ (k + 1)
case intro
β : Type ?u.39271
A : Type ?u.39274
G : Type ?u.39277
M : Type u_1
R : Type ?u.39283
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : M
n : ℕ
ha : 1 < a
k : ℕ
⊢ a ^ n < a ^ (Nat.succ n + k)
rw [pow_add, pow_succ', mul_assoc, ← pow_succ]
no goals
case intro
β : Type ?u.39271
A : Type ?u.39274
G : Type ?u.39277
M : Type u_1
R : Type ?u.39283
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : M
n : ℕ
ha : 1 < a
k : ℕ
⊢ a ^ n < a ^ n * a ^ (k + 1)
exact lt_mul_of_one_lt_right' _ (one_lt_pow' ha k.succ_ne_zero)