let a, k, n be Nat; :: thesis: ( a = n - 1 & k < n implies not not k = 0 & ... & not k = a )
assume ( a = n - 1 & k < n ) ; :: thesis: not not k = 0 & ... & not k = a
then k <= a by INT_1:52;
hence not not k = 0 & ... & not k = a ; :: thesis: verum