proposition: Lemma testbit_Zpos a n : 0<=n -> testbit (pos a) n = N.testbit (N.pos a) (to_N n).
proof: Proof. intro Hn. now rewrite <- testbit_of_N'. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass