no goals
β : Type ?u.157025
A : Type ?u.157028
G : Type ?u.157031
M : Type u_1
R : Type ?u.157037
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_lt_max_of_mul_lt_mul ((pow_two _).symm.trans_lt h)