for i being Integer st i <> 0 holds
i div i = 1 by Th45;