let nn, nn' be Nat; :: thesis: ( nn <> 0 & nn = 2 * nn' implies nn' < nn )
assume that
A1: nn <> 0 and
A2: nn = 2 * nn' and
A3: nn <= nn' ; :: thesis: contradiction

per cases ( nn = nn' or nn < nn' ) by A3, XXREAL_0:1;

suppose nn = nn' ; :: thesis: contradiction

hence contradiction by A1, A2; :: thesis: verum

end;

suppose nn < nn' ; :: thesis: contradiction

then (2 * nn') + (- (1 * nn')) < (1 * nn') + (- (1 * nn')) by A2, XREAL_1:8;
hence contradiction by NAT_1:2; :: thesis: verum

end;

end;