proposition: Lemma to_Z_rec_bounded size : forall x, (0 <= to_Z_rec size x < 2 ^ Z.of_nat size)%Z.
proof: Proof. elim size. - simpl; auto with zarith. - intros n ih x; rewrite inj_S; simpl; assert (W := ih (x >> 1)%uint63). rewrite Z.pow_succ_r; auto with zarith. destruct (is_even x). + rewrite Zdouble_mult; auto with zarith. + rewrite Zdouble_plus_one_mult; auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63