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