proposition: Lemma Zdiv_gcd_elim_rht : forall a b q : Z, Zdivides b q -> Zdivides (Zgcd a b) q.
proof: Proof. intros a b q Hdiv; apply (Zdivides_trans (Zgcd a b) b q); [ apply Zgcd_is_divisor_rht | assumption ]. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)