proposition: Lemma shift_equiv n p : 0<=n -> Zpos (shift n p) = Z.shiftl (Zpos p) n.
proof: Proof. destruct n. - trivial. - simpl; intros. now apply Pos.iter_swap_gen. - now destruct 1. Qed.
imports: Wf_nat ZArith_base Zcomplements Zpow_def