let a, b be positive Real; :: thesis: (a + b) / 2 >= sqrt (a * b)
(a + b) / 2 >= (2 * (sqrt (a * b))) / 2 by SIN_COS2:1, XREAL_1:72;
hence (a + b) / 2 >= sqrt (a * b) ; :: thesis: verum