proposition: Lemma testbit_ones_nonneg n i (Hn : 0 <= n) (Hi: 0 <= i) : testbit (ones n) i = (i <? n).
proof: Proof. rewrite testbit_ones by auto. destruct (leb_spec 0 i); cbn; solve [ trivial | destruct (proj1 (Z.le_ngt _ _) Hi ltac:(eassumption)) ]. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass