proposition: Lemma Zdiv_rest_ok x p : let (q,r) := Zdiv_rest x p in x = q * 2^(Zpos p) + r /\ 0 <= r < 2^(Zpos p).
proof: Proof. unfold Zdiv_rest. generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p). destruct (Pos.iter Zdiv_rest_aux (x, 0, 1) p) as ((q,r),d). intros H ->. now rewrite two_power_pos_equiv in H. Qed.
imports: Wf_nat ZArith_base Zcomplements Zpow_def