proposition: Lemma egcd_gcd_log2: forall c a b, match egcd_log2 a b c, gcd_log2 a b c with None, None => True | Some (u,v,r), Some r' => r = r' | _, _ => False end.
proof: Proof. induction c; simpl; auto; try (intros a b; generalize (Pmod_div_eucl a b); case (a/b); simpl; intros q r1 H; subst; case (a mod b); auto; intros r; generalize (Pmod_div_eucl b r); case (b/r); simpl; intros q' r1 H; subst; case (b mod r); auto; intros r'; generalize (IHc r r'); case egcd_log2; auto; intros ((p1,p2),p3); case gcd_log2; auto). Qed.
imports: ZArith Lia ZCmisc