let nn, nn9 be Nat; :: thesis: ( nn = (2 * nn9) + 1 implies nn9 < nn )
assume A1: nn = (2 * nn9) + 1 ; :: thesis: nn9 < nn
assume nn <= nn9 ; :: thesis: contradiction
then nn <= nn9 + nn9 by NAT_1:12;
hence contradiction by A1, NAT_1:13; :: thesis: verum