proposition: Lemma gcd_log2_mod : forall a b, Zpos b <= Zpos a -> forall r, a mod b = Npos r -> gcd_log2 a b b = gcd_log2 b r r.
proof: Proof. intros a b;generalize a;clear a; assert (Hacc := Zwf_pos b). induction Hacc; intros a Hle r Hmod. rename x into b. destruct b;simpl;rewrite Hmod. CaseEq (xI b mod r)%P;intros. rewrite gcd_log2_mod0;trivial. assert (H2 := mod_le _ _ _ H1);assert (H3 := mod_lt _ _ _ Hmod); assert (H4 := mod_le _ _ _ Hmod). rewrite (gcd_log2_Zle_log r p b);trivial. symmetry;apply H0;trivial. generalize (mod_log2 _ _ _ H1 H4);simpl;zsimpl;intros;lia. CaseEq (xO b mod r)%P;intros. rewrite gcd_log2_mod0;trivial. assert (H2 := mod_le _ _ _ H1);assert (H3 := mod_lt _ _ _ Hmod); assert (H4 := mod_le _ _ _ Hmod). rewrite (gcd_log2_Zle_log r p b);trivial. symmetry;apply H0;trivial. generalize (mod_log2 _ _ _ H1 H4);simpl;zsimpl;intros;lia. rewrite mod1 in Hmod;discriminate Hmod. Qed.
imports: ZArith Lia ZCmisc Zwf