proposition: Lemma egcd_Zis_gcd : forall a b:positive, let (uv,w) := egcd a b in let (u,v) := uv in u * a + v * b = w /\ (Zis_gcd b a w).
proof: Proof. Proof with mauto. intros a b; unfold egcd. generalize (egcd_log2_ok (xO b) a b) (egcd_gcd_log2 (xO b) a b) (egcd_log2_x0 a b) (gcd_Zis_gcd b a); unfold egcd, gcd. case egcd_log2; try (intros ((u,v),w)); case gcd_log2; try (intros; match goal with H: False |- _ => case H end); try (intros _ _ H1; case H1; auto; fail). intros; subst; split; try apply Zis_gcd_sym; auto. Qed.
imports: ZArith Lia ZCmisc Zwf ZArith Znumtheory