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

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

suppose nn = nn9 ; :: thesis: contradiction

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

end;

suppose nn < nn9 ; :: thesis: contradiction

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

end;

end;