per cases ( n is zero or not n is zero ) ;

suppose n is zero ; :: thesis: n choose 1 = n

hence n choose 1 = n by NEWTON:def 3; :: thesis: verum

end;

suppose not n is zero ; :: thesis: n choose 1 = n

hence n choose 1 = n by NEWTON:23, NAT_1:14; :: thesis: verum

end;

end;