for a being Integer holds
( a divides 0 & 1 divides a & - 1 divides a ) by Lm5;