let n be Nat; :: thesis: (1 / (n + 1)) - (3 / ((n + 1) * (n + 4))) = 1 / (n + 4)
n >= 0 by NAT_1:2;
then A1: n + 1 > 0 by NAT_1:13;
then (n + 1) + 1 > 0 by NAT_1:13;
then (n + 2) + 1 > 0 by NAT_1:13;
then (n + 3) + 1 > 0 by NAT_1:13;
then (1 / (n + 1)) - (3 / ((n + 1) * (n + 4))) = ((1 * (n + 4)) / ((n + 1) * (n + 4))) - (3 / ((n + 1) * (n + 4))) by XCMPLX_1:91
.= ((n + 4) - 3) / ((n + 1) * (n + 4)) by XCMPLX_1:120
.= ((n + 1) * 1) / ((n + 1) * (n + 4))
.= 1 / (n + 4) by A1, XCMPLX_1:91 ;
hence (1 / (n + 1)) - (3 / ((n + 1) * (n + 4))) = 1 / (n + 4) ; :: thesis: verum