let n be Nat; :: thesis: 1 / ((2 -Root (n + 2)) + (2 -Root (n + 1))) = (2 -Root (n + 2)) - (2 -Root (n + 1))
(n + 1) + 1 > n + 1 by NAT_1:13;
then 2 -Root (n + 2) > 2 -Root (n + 1) by PREPOWER:28;
then (2 -Root (n + 2)) - (2 -Root (n + 1)) > (2 -Root (n + 1)) - (2 -Root (n + 1)) by XREAL_1:9;
then (1 / ((2 -Root (n + 2)) + (2 -Root (n + 1)))) * 1 = (1 * ((2 -Root (n + 2)) - (2 -Root (n + 1)))) / (((2 -Root (n + 2)) - (2 -Root (n + 1))) * ((2 -Root (n + 2)) + (2 -Root (n + 1)))) by XCMPLX_1:91
.= ((2 -Root (n + 2)) - (2 -Root (n + 1))) / (((2 -Root (n + 2)) |^ 2) - ((2 -Root (n + 1)) |^ 2)) by Lm4
.= ((2 -Root (n + 2)) - (2 -Root (n + 1))) / ((n + 2) - ((2 -Root (n + 1)) |^ 2)) by PREPOWER:19
.= ((2 -Root (n + 2)) - (2 -Root (n + 1))) / ((n + 2) - (n + 1)) by PREPOWER:19
.= (2 -Root (n + 2)) - (2 -Root (n + 1)) ;
hence 1 / ((2 -Root (n + 2)) + (2 -Root (n + 1))) = (2 -Root (n + 2)) - (2 -Root (n + 1)) ; :: thesis: verum