proposition: Lemma ones_spec n m: 0 ≤ m → 0 ≤ n → Z.testbit (Z.ones n) m = bool_decide (m < n).
proof: Proof. intros. case_bool_decide. - by rewrite Z.ones_spec_low by lia. - by rewrite Z.ones_spec_high by lia. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)