for m, n being Nat holds
( m divides n iff m divides n ) ;