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