proposition: Lemma testbit_odd_succ a n : 0<=n -> testbit (2*a+1) (succ n) = testbit a n.
proof: Proof. intros H. rewrite testbit_succ_r_div2 by trivial. f_equal. now destruct a. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties