theorem :: NAT_LAT:3

for a, b being Element of Nat_Lattice st a [= b holds
a divides b by NEWTON:44;