have habc : a * b * c > 0 := Real.mul_pos (Real.mul_pos ha hb) hc
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)