proposition: Lemma testbit_succ_r a (b:bool) n : testbit (2*a+b) (succ n) = testbit a n.
proof: Proof. destruct b; simpl; rewrite ?add_0_r. - apply testbit_odd_succ, le_0_l. - apply testbit_even_succ, le_0_l. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog