proposition: Lemma Zgcd_is_divisor : forall a b : Z, Zdivides (Zgcd a b) a.
proof: Proof. intros a b. case a. auto with zarith. case b. auto with zarith. intros pb pa; generalize (p_gcd_is_divisor pa pb); tauto. intros pb pa; generalize (p_gcd_is_divisor pa pb); tauto. case b. auto with zarith. intros pb pa; generalize (p_gcd_is_divisor pa pb); intro H. apply Zdivides_opp_intro_rht; simpl in |- *. tauto. intros pb pa; generalize (p_gcd_is_divisor pa pb); intro H. apply Zdivides_opp_intro_rht; simpl in |- *. tauto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)