proposition: Lemma Zdiv_gcd_elim : forall a b q : Z, Zdivides q a -> Zdivides q b -> Zdivides q (Zgcd a b).
proof: Proof. intros a b q Ha Hb. cut (a <> 0%Z \/ b <> 0%Z -> Zdivides q (Zgcd a b)). case (Zdec a); case (Zdec b); auto. intros Hb0 Ha0; rewrite Ha0 in Ha; rewrite Ha0; rewrite Hb0. rewrite Zgcd_zero_rht; auto. intro Hnon0; generalize (Zgcd_is_gcd a b); unfold Zis_gcd in |- *; intro H; elim H; clear H; intros H0 H1; elim H1; clear H1. intros _ H1; elim H1; clear H1; intros _ H1; elim H1; clear H1; intros _ Hdiv. generalize (Hdiv q); intro Hq; auto. auto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)