let n be Nat; :: thesis: (Triangle (n -' 1)) + (Triangle n) = n ^2

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

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

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

end;

suppose A2: n = 0 ; :: thesis: (Triangle (n -' 1)) + (Triangle n) = n ^2

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

end;

end;