proposition: Lemma shiftr_spec a n m : 0<=m -> testbit (shiftr a n) m = testbit a (m+n).
proof: Proof. intros _. revert a m. induction n as [|n IHn] using peano_ind; intros a m. - now rewrite add_0_r. - rewrite add_comm, add_succ_l, add_comm, <- add_succ_l. now rewrite <- IHn, testbit_succ_r_div2, shiftr_succ_r by apply le_0_l. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties