proposition: Lemma testbit_of_N a n : testbit (of_N a) (of_N n) = N.testbit a n.
proof: Proof. destruct a as [|a], n; simpl; trivial. now destruct a. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass