proposition: Lemma bounded_iff_bits_nonneg' k n : 0 ≤ k → 0 ≤ n → 0 ≤ n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false.
proof: Proof. intros ??. rewrite <-bounded_iff_bits_nonneg; lia. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)