let n be Nat; :: thesis: Triangle (n -' 1) = (n * (n - 1)) / 2

per cases ( n <> 0 or n = 0 ) ;

suppose n <> 0 ; :: thesis: Triangle (n -' 1) = (n * (n - 1)) / 2

then A1: 1 <= 1 * n by Th1;
Triangle (n -' 1) = ((n -' 1) * ((n -' 1) + 1)) / 2 by Th19
.= ((n -' 1) * n) / 2 by XREAL_1:235, A1 ;
hence Triangle (n -' 1) = (n * (n - 1)) / 2 by XREAL_1:233, A1; :: thesis: verum

end;

suppose A2: n = 0 ; :: thesis: Triangle (n -' 1) = (n * (n - 1)) / 2

then Triangle (n -' 1) = Triangle 0 by XREAL_0:def 2, Lm3
.= (n * (n - 1)) / 2 by A2 ;
hence Triangle (n -' 1) = (n * (n - 1)) / 2 ; :: thesis: verum

end;

end;