proposition: Lemma positive_to_int_spec : forall p : positive, Zpos p = Z_of_N (fst (positive_to_int p)) * wB + to_Z (snd (positive_to_int p)).
proof: Proof. assert (H: (wB <= wB) -> forall p : positive, Zpos p = Z_of_N (fst (positive_to_int p)) * wB + φ (snd (positive_to_int p)) /\ φ (snd (positive_to_int p)) < wB). 2: intros p; case (H (Z.le_refl wB) p); auto. unfold positive_to_int, wB at 1 3 4. elim size. - intros _ p; simpl; rewrite to_Z_0, Pmult_1_r; split; auto with zarith; apply refl_equal. - intros n; rewrite inj_S; unfold Z.succ; rewrite Zpower_exp, Z.pow_1_r; auto with zarith. intros IH Hle p. assert (F1: 2 ^ Z_of_nat n <= wB); auto with zarith. assert (0 <= 2 ^ Z_of_nat n); auto with zarith. case p; simpl. + intros p1. generalize (IH F1 p1); case positive_to_int_rec; simpl. intros n1 i (H1,H2). rewrite Zpos_xI, H1. replace (φ (i << 1 + 1)) with (φ i * 2 + 1). * split; auto with zarith; ring. * rewrite add_spec, lsl_spec, Zplus_mod_idemp_l, to_Z_1, Z.pow_1_r, Zmod_small; auto. case (to_Z_bounded i); split; auto with zarith. + intros p1. generalize (IH F1 p1); case positive_to_int_rec; simpl. intros n1 i (H1,H2). rewrite Zpos_xO, H1. replace (φ (i << 1)) with (φ i * 2). * split; auto with zarith; ring. * rewrite lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; auto. case (to_Z_bounded i); split; auto with zarith. + rewrite to_Z_1; assert (0 < 2^ Z_of_nat n); auto with zarith. Qed.
imports: CyclicAxioms ZArith Uint63