proposition: Lemma lt_pow_lt_log d k n : 0 < d <= n → 0 <= k < 2 ^ d → Z.log2 k < n.
proof: Proof. intros [hd hdn] [hk hkd]. assert (k = 0 ∨ 0 < k) as D by lia. clear hk; destruct D as [ hk | hk ]. - subst k; simpl; lia. - apply Z.log2_lt_pow2. + lia. + eapply Z.lt_le_trans. * eassumption. * apply Z.pow_le_mono_r; lia. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63