let n be natural even number ; :: thesis: n div 2 = n / 2
consider k being Nat such that
A1: n = 2 * k by ABIAN:def 2;
thus n div 2 = n / 2 by A1, INT_1:25; :: thesis: verum