let a, b be positive Real; :: thesis: (b / a) + (a / b) >= 2
(a - b) ^2 >= 0 by XREAL_1:63;
then (((a ^2) - ((2 * a) * b)) + (b ^2)) + ((2 * a) * b) >= 0 + ((2 * a) * b) by XREAL_1:7;
then ((a ^2) + (b ^2)) / (a * b) >= (2 * (a * b)) / (1 * (a * b)) by XREAL_1:72;
then A1: ((a ^2) + (b ^2)) / (a * b) >= 2 / 1 by XCMPLX_1:91;
(b / a) + (a / b) = ((b * b) / (a * b)) + (a / b) by XCMPLX_1:91
.= ((b * b) / (a * b)) + ((a * a) / (a * b)) by XCMPLX_1:91
.= ((b ^2) + (a ^2)) / (a * b) ;
hence (b / a) + (a / b) >= 2 by A1; :: thesis: verum