proposition: Lemma testbit_odd_succ a n : 0<=n -> testbit (2*a+1) (succ n) = testbit a n.
proof: Proof. destruct n as [|n|n]; (now destruct 1) || intros _. - destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a. - unfold testbit; simpl. destruct a as [|a|[a|a|]]; simpl; trivial; rewrite ?Pos.add_1_r, ?Pos.pred_N_succ; now destruct n. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass