proposition: Lemma gcd_log2_Zle_log : forall a b c, log2 b <= log2 c -> Zpos b <= Zpos a -> gcd_log2 a b c = gcd_log2 a b b.
proof: Proof. intros a b c H1 H2; apply gcd_log2_Zle; trivial. apply gcd_log2_None; trivial. Qed.
imports: ZArith Lia ZCmisc