theorem zdvdtr (a b c: nat): $ a |Z b -> b |Z c -> a |Z c $;
zabs a || zabs b -> zabs b || zabs c -> zabs a || zabs c
a |Z b -> b |Z c -> a |Z c