k + n <> 1 by NAT_1:12, NAT_2:29;
hence ( not k + n is trivial & not k + n is zero ) by NAT_2:def 1; :: thesis: verum