proposition: Lemma of_pos_rec_spec (k: nat) : (k <= size)%nat → ∀ p, φ(of_pos_rec k p) = Zpos p mod 2 ^ Z.of_nat k.
proof: Proof. elim k; clear k. { intros _ [p|p| ]; simpl; rewrite to_Z_0, Zmod_1_r; reflexivity. } intros n ih hn. assert (n <= size)%nat as hn' by lia. specialize (ih hn'). intros [ p | p | ]. 3: { rewrite Zmod_small. - reflexivity. - split. + lia. + apply Zpower_gt_1; lia. } - simpl. destruct (bit_add_or (of_pos_rec n p << 1) 1) as (H1, _). rewrite <- H1;clear H1. 2: { intros i; rewrite bit_lsl, bit_1. case eqbP. + intros h; apply to_Z_inj in h; subst. exact (λ e _, diff_false_true e). + exact (λ _ _, diff_false_true). } rewrite add_spec, lsl_spec, ih, to_Z_1; clear ih. rewrite Z.pow_pos_fold, Zpos_P_of_succ_nat. change (Zpos p~1) with (2 ^ 1 * Zpos p + 1)%Z. rewrite Zmod_distr by lia. rewrite Zpower_Zsucc by auto with zarith. rewrite Zplus_mod_idemp_l. rewrite Zmod_small. { rewrite Zmult_mod_distr_l; lia. } set (a := Z.of_nat n). set (b := Zpos p). change (2 ^ 1) with 2. pose proof (pow2_pos a (Nat2Z.is_nonneg _)). elim_div; intros x y [ ? ha]. { lia. } destruct ha as [ ha | ]. 2: lia. split. { lia. } apply Z.lt_le_trans with (2 ^ (a + 1)). 2: apply Z.pow_le_mono_r; subst a; lia. fold (Z.succ a); rewrite Z.pow_succ_r. { lia. } subst a; lia. - simpl. rewrite lsl_spec, ih, to_Z_1, Zmod_small. + rewrite Z.pow_pos_fold, Zpos_P_of_succ_nat, Zpower_Zsucc by lia. change (Zpos p~0) with (2 ^ 1 * Zpos p)%Z. rewrite Z.mul_mod_distr_l; auto with zarith. + set (a := Z.of_nat n). set (b := Zpos p). change (2 ^ 1) with 2. pose proof (pow2_pos a (Nat2Z.is_nonneg _)). elim_div; intros x y [ ? ha]. { lia. } destruct ha as [ ha | ]. 2: lia. split. { lia. } apply Z.lt_le_trans with (2 ^ (a + 1)). 2: apply Z.pow_le_mono_r; subst a; lia. fold (Z.succ a); rewrite Z.pow_succ_r. { lia. } subst a; lia. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63