proposition: Lemma Zdiv_rest_shiftr x p : fst (Zdiv_rest x p) = Z.shiftr x (Zpos p).
proof: Proof. generalize (Zdiv_rest_ok x p). destruct (Zdiv_rest x p) as (q,r). intros (H,H'). simpl. rewrite Z.shiftr_div_pow2 by easy. apply Z.div_unique_pos with r; trivial. now rewrite Z.mul_comm. Qed.
imports: Wf_nat ZArith_base Zcomplements Zpow_def