proposition: Lemma gcd_Zis_gcd : forall a b:positive, (Zis_gcd b a (gcd b a)%P).
proof: Proof. Proof with mauto. intros a;assert (Hacc := Zwf_pos a);induction Hacc;rename x into a;intros. generalize (div_eucl_spec b a)... rewrite <- (Pmod_div_eucl b a). CaseEq (b mod a)%P;[intros Heq|intros r Heq]; intros (H1,H2). simpl in H1;rewrite Zplus_0_r in H1. rewrite (gcd_mod0 _ _ Heq). constructor;mauto. apply Zdivide_intro with (fst (b/a)%P);trivial. rewrite (gcd_mod _ _ _ Heq). rewrite H1;apply Zis_gcd_sym. rewrite Zmult_comm;apply Zis_gcd_for_euclid2;simpl in *. apply Zis_gcd_sym;auto. Qed.
imports: ZArith Lia ZCmisc Zwf ZArith Znumtheory