let a be positive Real; :: thesis: for n being Nat holds [\(n * a)/] >= n * [\a/]
let n be Nat; :: thesis: [\(n * a)/] >= n * [\a/]

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: [\(n * a)/] >= n * [\a/]

hence [\(n * a)/] >= n * [\a/] ; :: thesis: verum

end;

suppose A0: n <> 0 ; :: thesis: [\(n * a)/] >= n * [\a/]

A1: ( a - 1 <= [\a/] & [\a/] <= a & (n * a) - 1 <= [\(n * a)/] & [\(n * a)/] <= n * a ) by INT_1:def 6;
then A2: ((n * a) - 1) + 1 <= [\(n * a)/] + 1 by XREAL_1:6;

per cases ( [\a/] = a or [\a/] < a ) by A1, XXREAL_0:1;

suppose [\a/] = a ; :: thesis: [\(n * a)/] >= n * [\a/]

hence [\(n * a)/] >= n * [\a/] ; :: thesis: verum

end;

suppose [\a/] < a ; :: thesis: [\(n * a)/] >= n * [\a/]

then n * [\a/] < n * a by A0, XREAL_1:68;
then n * [\a/] < [\(n * a)/] + 1 by A2, XXREAL_0:2;
hence [\(n * a)/] >= n * [\a/] by INT_1:7; :: thesis: verum

end;

end;

end;

end;