proposition: Lemma testbit_0_r a (b:bool) : testbit (2*a+b) 0 = b.
proof: Proof. destruct b; simpl; rewrite ?add_0_r. - apply testbit_odd_0. - apply testbit_even_0. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog