proposition: Lemma Zegcd_is_egcd : forall x y, match Zegcd x y with (u,v,w) => u * x + v * y = w /\ Zis_gcd x y w /\ 0 <= w end.
proof: Proof. assert (zx0: forall x, Zneg x = -x). simpl; auto. assert (zx1: forall x, -(-x) = x). intro x; case x; simpl; auto. destruct x;destruct y;simpl; try (split; [idtac|split]); auto; try (red; simpl; intros; discriminate); try (rewrite zx0; apply Zis_gcd_minus; try rewrite zx1; auto; apply Zis_gcd_minus; try rewrite zx1; simpl; auto); try apply Zis_gcd_0; try (apply Zis_gcd_sym;apply Zis_gcd_0); generalize (egcd_Zis_gcd p p0); case egcd; intros (u,v) w (H1, H2); split; repeat rewrite zx0; try (rewrite <- H1; ring); auto; (split; [idtac | red; intros; discriminate]). apply Zis_gcd_sym; auto. apply Zis_gcd_sym; apply Zis_gcd_minus; rw zx1; apply Zis_gcd_sym; auto. apply Zis_gcd_minus; rw zx1; auto. apply Zis_gcd_minus; rw zx1; auto. apply Zis_gcd_minus; rw zx1; auto. apply Zis_gcd_sym; auto. Qed.
imports: ZArith Lia ZCmisc Zwf ZArith Znumtheory