let n be Nat; :: thesis: for i being Integer st n divides i holds
i div n = i / n
let i be Integer; :: thesis: ( n divides i implies i div n = i / n )
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: ( n divides i implies i div n = i / n )
hence ( n divides i implies i div n = i / n ) by INT_1:48; :: thesis: verum
end;
suppose A1: n <> 0 ; :: thesis: ( n divides i implies i div n = i / n )
assume A2: n divides i ; :: thesis: i div n = i / n
i mod n = 0 by A1, A2, INT_1:62;
hence i div n = i / n by A1, PEPIN:63; :: thesis: verum
end;
end;