proposition: Lemma testbit_succ_r_div2 a n : 0<=n -> testbit a (succ n) = testbit (div2 a) n.
proof: Proof. intros _. destruct a as [|[a|a| ]], n as [|n]; simpl; trivial; f_equal; apply Pos.pred_N_succ. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties