proposition: Lemma gcd_log2_None_aux : forall c a b, Zpos b <= Zpos a -> log2 b <= log2 c -> gcd_log2 a b c <> None.
proof: Proof. induction c;simpl;intros; (CaseEq (a mod b);[intros Heq|intros r Heq];try (intro;discriminate)); (CaseEq (b mod r);[intros Heq'|intros r' Heq'];try (intro;discriminate)). apply IHc. apply mod_le with b;trivial. generalize H0 (mod_log2 _ _ _ Heq' (mod_le _ _ _ Heq));zsimpl;intros;lia. apply IHc. apply mod_le with b;trivial. generalize H0 (mod_log2 _ _ _ Heq' (mod_le _ _ _ Heq));zsimpl;intros;lia. assert (Zpos (log2 b) = 1). assert (H1 := Zlt_0_pos (log2 b));lia. rewrite (log2_1_inv _ H1) in Heq;rewrite mod1 in Heq;discriminate Heq. Qed.
imports: ZArith Lia ZCmisc