proposition: Lemma testbit_odd_succ' a n : testbit (2*a+1) (S n) = testbit a n.
proof: Proof. unfold testbit; fold testbit. rewrite add_1_r; f_equal. apply div2_succ_double. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass