let n be Nat; :: thesis: ( n <> 0 implies n < 2 * n )
assume that
A1: n <> 0 and
A2: 2 * n <= n ; :: thesis: contradiction

per cases ( 2 * n = n or 2 * n < n ) by A2, XXREAL_0:1;

suppose 2 * n = n ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose 2 * n < n ; :: thesis: contradiction

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

end;

end;