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

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

suppose nn = nn' ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose nn < nn' ; :: thesis: contradiction

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

end;

end;