********************************************************************************
*                                                                              *
*  To show n - i <= n - 1, consider rule inequals(82), instantiated with       *
*  A=n, B=n, C=1, D=i, giving:                                                 *
*                                                       (1)     (2)            *
*      inequals(82): n-i <= n-1 may_be_deduced_from [ n <= n, 1 <= i ].        *
*                                                                              *
*  Clearly, (1) n <= n holds, and (2) 1 <= i is just i >= 1 (which we know     *
*  holds) written another way.                                                 *
*                                                                              *
*  Next, to show j + 1 <= n, consider rule inequals(65), instantiated with     *
*  I=j, J=n-1, N=1; this gives:                                                *
*                                                    (1)         (2)           *
*      inequals(65): j+1 <= n may_be_deduced_from [ n = n-1+1, j <= n-1 ].     *
*                                                                              *
*  (1) is simple enough for the Checker's inference engine (with               *
*  simplification) to handle, while (2) follows from j <= n-i (which we know)  *
*  and n-i <= n-1 (from the above reasoning, with inequals(82)).               *
*                                                                              *
********************************************************************************