proposition: Lemma gcd_log2_xO_Zle : forall a b, Zpos b <= Zpos a -> gcd_log2 a b (xO b) = gcd_log2 a b b.
proof: Proof. intros a b Hle;apply gcd_log2_Zle. simpl;zsimpl;auto with zarith. apply gcd_log2_None_aux;auto with zarith. Qed.
imports: ZArith Lia ZCmisc Zwf