let n, a be non zero Nat; :: thesis: ( a divides n implies n div a <> 0 )
assume A0: a divides n ; :: thesis: n div a <> 0
assume n div a = 0 ; :: thesis: contradiction
then n < a by NAT_2:12;
hence contradiction by NAT_D:7, A0; :: thesis: verum