no goals
β : Type ?u.151798
A : Type ?u.151801
G : Type ?u.151804
M : Type u_1
R : Type ?u.151810
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_lt_max_of_mul_lt_mul (h.trans_eq <| pow_two _)