proposition: Lemma bounded_iff_bits_nonneg k n : 0 ≤ k → 0 ≤ n → n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false.
proof: Proof. intros. destruct (decide (n = 0)) as [->|]. { naive_solver eauto using Z.bits_0, Z.pow_pos_nonneg with lia. } split. { intros Hb%Z.log2_lt_pow2 l Hl; [|lia]. apply Z.bits_above_log2; lia. } intros Hl. apply Z.nle_gt; intros ?. assert (Z.testbit n (Z.log2 n) = false) as Hbit. { apply Hl, Z.log2_le_pow2; lia. } by rewrite Z.bit_log2 in Hbit by lia. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)