proposition: Lemma gcd_log2_xO_Zlt : forall a b, Zpos a < Zpos b -> gcd_log2 a b (xO b) = gcd_log2 b a a.
proof: Proof. intros a b H;simpl. assert (Hlt := Zlt_0_pos a). assert (H0 := lt_mod _ _ H). rewrite H0;simpl. CaseEq (b mod a)%P;intros;simpl. symmetry;apply gcd_log2_mod0;trivial. assert (H2 := mod_lt _ _ _ H1). rewrite (gcd_log2_Zle_log a p b);auto with zarith. symmetry;apply gcd_log2_mod;auto with zarith. apply log2_Zle. replace (Zpos p) with (Z_of_N (Npos p));trivial. apply mod_le_a with a;trivial. Qed.
imports: ZArith Lia ZCmisc Zwf