proposition: Lemma Zmodeq_trans : forall a b c : Z, Zmodeq b a -> Zmodeq a c -> Zmodeq b c.
proof: Proof. unfold Zmodeq in |- *. intros. replace (b - c)%Z with (b - a + (a - c))%Z; auto with zarith. Qed.
imports: CoRN.model.Zmod.ZGcd