proposition: Lemma shiftr_spec a n m : 0<=m -> testbit (shiftr a n) m = testbit a (m+n).
proof: Proof. intros Hm. destruct (leb_spec 0 n). - now apply shiftr_spec_aux. - destruct (leb_spec (-n) m) as [LE|GT]. + unfold shiftr. rewrite (shiftl_spec_high a (-n) m); trivial. now destruct n. + unfold shiftr. rewrite (shiftl_spec_low a (-n) m); trivial. rewrite testbit_neg_r; trivial. red in GT. rewrite compare_sub in GT. now destruct n. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass