let k, n be Nat; :: thesis: ( k <= n implies not not k = 0 & ... & not k = n )
thus ( k <= n implies not not k = 0 & ... & not k = n ) ; :: thesis: verum