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 ) ; :: 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 PEPIN:63; :: thesis: verum

end;

end;