proposition: Lemma Zdivides_trans : forall a b c : Z, Zdivides a b -> Zdivides b c -> Zdivides a c.
proof: Proof. intros. unfold Zdivides in H; elim H; intros. unfold Zdivides in H0; elim H0; intros. exists (x0 * x)%Z. rewrite <- H2. rewrite <- H1. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZBasics