proposition: Lemma Zgcd_is_gcd : forall a b : Z, Zis_gcd a b (Zgcd a b).
proof: Proof. intros a b. unfold Zis_gcd in |- *. split. intros Ha Hb; rewrite Ha; rewrite Hb; auto with zarith. intros Hab. split. generalize (Zgcd_pos a b Hab); auto with zarith. split. apply Zgcd_is_divisor_lft. split. apply Zgcd_is_divisor_rht. intros q Hq. rewrite Zgcd_lin_comb. apply Zdivides_plus_elim. apply Zdivides_mult_elim_lft; tauto. apply Zdivides_mult_elim_lft; tauto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)