proposition: Lemma shiftr_spec_aux a n m : 0<=n -> 0<=m -> testbit (shiftr a n) m = testbit a (m+n).
proof: Proof. intros Hn Hm. unfold shiftr. destruct n as [ |n|n]; (now destruct Hn) || clear Hn; simpl. - now rewrite add_0_r. - assert (forall p, to_N (m + pos p) = (to_N m + N.pos p)%N) as H by (destruct m; trivial; now destruct Hm). assert (forall p, 0 <= m + pos p) by (destruct m; easy || now destruct Hm). destruct a as [ |a|a]. + replace (Pos.iter div2 0 n) with 0 by (apply Pos.iter_invariant; intros; subst; trivial). now rewrite 2 testbit_0_l. + change (pos a) with (of_N (N.pos a)) at 1. rewrite <- (Pos.iter_swap_gen _ _ _ N.div2) by now intros [|[ | | ]]. rewrite testbit_Zpos, testbit_of_N', H; trivial. exact (N.shiftr_spec' (N.pos a) (N.pos n) (to_N m)). + rewrite <- (Pos.iter_swap_gen _ _ _ Pos.div2_up) by trivial. rewrite 2 testbit_Zneg, H; trivial. f_equal. rewrite (Pos.iter_swap_gen _ _ _ _ N.div2) by exact N.pred_div2_up. exact (N.shiftr_spec' (Pos.pred_N a) (N.pos n) (to_N m)). Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass