let b, a be real positive number ; :: thesis: (b / a) + (a / b) >= 2
(a - b) ^2 >= 0 by XREAL_1:65;
then (((a ^2 ) - ((2 * a) * b)) + (b ^2 )) + ((2 * a) * b) >= 0 + ((2 * a) * b) by XREAL_1:9;
then ((a ^2 ) + (b ^2 )) / (a * b) >= (2 * (a * b)) / (1 * (a * b)) by XREAL_1:74;
then A1: ((a ^2 ) + (b ^2 )) / (a * b) >= 2 / 1 by XCMPLX_1:92;
(b / a) + (a / b) = ((b * b) / (a * b)) + (a / b) by XCMPLX_1:92
.= ((b * b) / (a * b)) + ((a * a) / (a * b)) by XCMPLX_1:92
.= ((b ^2 ) + (a ^2 )) / (a * b) ;
hence (b / a) + (a / b) >= 2 by A1; :: thesis: verum