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