proposition: Lemma gcd_log2_x0 : forall a b, gcd_log2 a b (xO b) <> None.
proof: Proof. intros;simpl;CaseEq (a mod b)%P;intros. intro;discriminate. CaseEq (b mod p)%P;intros. intro;discriminate. assert (H1 := mod_le_a _ _ _ H0). unfold Z_of_N in H1. assert (H2 := mod_le _ _ _ H0). apply gcd_log2_None_aux. trivial. apply log2_Zle. trivial. Qed.
imports: ZArith Lia ZCmisc Zwf