let n be Nat; :: thesis: (n + 1) choose 2 = (n * (n + 1)) / 2
per cases ( n <> 0 or n = 0 ) ;
suppose A1: n <> 0 ; :: thesis: (n + 1) choose 2 = (n * (n + 1)) / 2
then A2: n = (n -' 1) + 1 by XREAL_1:235, NAT_1:14;
A3: n + 1 >= 1 + 1 by NAT_1:14, A1, XREAL_1:6;
n -' 1 = n - 1 by XREAL_1:233, NAT_1:14, A1
.= (n + 1) - 2 ;
then (n + 1) choose 2 = ((n + 1) !) / ((2 !) * ((n -' 1) !)) by NEWTON:def 3, A3
.= ((n !) * (n + 1)) / (2 * ((n -' 1) !)) by NEWTON:15, NEWTON:14
.= ((((n -' 1) !) * n) * (n + 1)) / (2 * ((n -' 1) !)) by NEWTON:15, A2
.= (((n -' 1) !) * (n * (n + 1))) / (2 * ((n -' 1) !))
.= (n * (n + 1)) / 2 by XCMPLX_1:91 ;
hence (n + 1) choose 2 = (n * (n + 1)) / 2 ; :: thesis: verum
end;
suppose n = 0 ; :: thesis: (n + 1) choose 2 = (n * (n + 1)) / 2
hence (n + 1) choose 2 = (n * (n + 1)) / 2 by NEWTON:def 3; :: thesis: verum
end;
end;