no goals
β : Type ?u.175159
A : Type ?u.175162
G : Type ?u.175165
M : Type u_1
R : Type ?u.175171
inst✝³ : Monoid M
inst✝² : LinearOrder M
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
a b c : M
h : a ^ 2 ≤ b * c
⊢ a ≤ max b c
simpa using min_le_max_of_mul_le_mul ((pow_two _).symm.trans_le h)