proposition: Lemma Zdiv_rest_correct1 (x:Z) (p:positive) : let (_, d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in d = two_power_pos p.
proof: Proof. rewrite Pos2Nat.inj_iter, two_power_pos_nat. induction (Pos.to_nat p); simpl; trivial. destruct (nat_rect _ _ _ _) as ((q,r),d). unfold Zdiv_rest_aux. rewrite two_power_nat_S; now f_equal. Qed.
imports: Wf_nat ZArith_base Zcomplements Zpow_def