proposition: Lemma Zgcd_is_gcd : forall x y, Zis_gcd x y (Zgcd x y).
proof: Proof. destruct x;destruct y;simpl. apply Zis_gcd_0. apply Zis_gcd_sym;apply Zis_gcd_0. apply Zis_gcd_sym;apply Zis_gcd_0. apply Zis_gcd_0. apply gcd_Zis_gcd. apply Zis_gcd_sym;apply Zis_gcd_minus;simpl;apply gcd_Zis_gcd. apply Zis_gcd_0. apply Zis_gcd_minus;simpl;apply Zis_gcd_sym;apply gcd_Zis_gcd. apply Zis_gcd_minus;apply Zis_gcd_minus;simpl;apply gcd_Zis_gcd. Qed.
imports: ZArith Lia ZCmisc Zwf ZArith Znumtheory