proposition: Lemma shiftr_specif : forall a n m, testbit (shiftr a n) m = testbit a (m+n).
proof: Proof. intros a n; induction n as [|n IHn]; intros m. - now rewrite add_0_r. - now rewrite add_succ_r, <- add_succ_l, <- IHn. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass