proposition: Lemma testbit_mod_pow2 a n i (H : 0 <= n) : testbit (a mod 2 ^ n) i = ((i <? n) && testbit a i)%bool.
proof: Proof. destruct (ltb_spec i n); rewrite ?mod_pow2_bits_low, ?mod_pow2_bits_high by auto; auto. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass