per cases ( a is zero or not a is zero ) ;

suppose a is zero ; :: thesis: [/a\] is zero

hence [/a\] is zero ; :: thesis: verum

end;

suppose not a is zero ; :: thesis: [/a\] is zero

then reconsider a = a as negative light Real ;
not a is integer ;
then [/a\] = [\a/] + 1 by INT_1:41, INT_1:34
.= (- 1) + 1 by TA1 ;
hence [/a\] is zero ; :: thesis: verum

end;

end;