no goals
β : Type ?u.169935
A : Type ?u.169938
G : Type ?u.169941
M : Type u_1
R : Type ?u.169947
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 * b ≤ c ^ 2
⊢ min a b ≤ c
simpa using min_le_max_of_mul_le_mul (h.trans_eq <| pow_two _)