let n be Nat; :: thesis: for i being Integer holds i div (i gcd n) = i / (i gcd n)
let i be Integer; :: thesis: i div (i gcd n) = i / (i gcd n)
( i gcd n divides i & i gcd n divides n ) by INT_2:def 2;
hence i div (i gcd n) = i / (i gcd n) by Th6; :: thesis: verum