no goals
β : Type u_1
A : Type ?u.67813
G : Type ?u.67816
M : Type u_2
R : Type ?u.67822
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
f : β → M
hf : StrictMono f
x✝ : 1 ≠ 0
⊢ StrictMono fun a => f a ^ 1
simpa
β : Type u_1
A : Type ?u.67813
G : Type ?u.67816
M : Type u_2
R : Type ?u.67822
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
f : β → M
hf : StrictMono f
n : ℕ
x✝ : Nat.succ (Nat.succ n) ≠ 0
⊢ StrictMono fun a => f a * f a ^ (n + 1)
β : Type u_1
A : Type ?u.67813
G : Type ?u.67816
M : Type u_2
R : Type ?u.67822
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
f : β → M
hf : StrictMono f
n : ℕ
x✝ : Nat.succ (Nat.succ n) ≠ 0
⊢ StrictMono fun a => f a ^ Nat.succ (Nat.succ n)
simp_rw [pow_succ _ (n + 1)]
no goals
β : Type u_1
A : Type ?u.67813
G : Type ?u.67816
M : Type u_2
R : Type ?u.67822
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
f : β → M
hf : StrictMono f
n : ℕ
x✝ : Nat.succ (Nat.succ n) ≠ 0
⊢ StrictMono fun a => f a * f a ^ (n + 1)
exact hf.mul' (StrictMono.pow_right' hf n.succ_ne_zero)