proposition: Lemma bit_0_spec i: φ (bit i 0) = φ i mod 2.
proof: Proof. unfold bit, is_zero. rewrite lsr_0_r. assert (Hbi: (φ i mod 2 < 2)%Z). { apply Z_mod_lt; auto with zarith. } case (to_Z_bounded i); intros H1i H2i. case (Z.mod_bound_pos_le (φ i) 2); auto with zarith; intros H3i H4i. assert (H2b: (0 < 2 ^ φ (digits - 1))%Z). { apply Zpower_gt_0; auto with zarith. case (to_Z_bounded (digits -1)); auto with zarith. } assert (H: φ (i << (digits -1)) = (φ i mod 2 * 2^ φ (digits -1))%Z). { rewrite lsl_spec. rewrite -> (Z_div_mod_eq_full φ i 2) at 1. rewrite -> Zmult_plus_distr_l, <-Zplus_mod_idemp_l. rewrite -> (Zmult_comm 2), <-Zmult_assoc. replace (2 * 2 ^ φ (digits - 1))%Z with wB; auto. rewrite Z_mod_mult, Zplus_0_l; apply Zmod_small. split; auto with zarith. replace wB with (2 * 2 ^ φ (digits -1))%Z; auto. apply Zmult_lt_compat_r; auto with zarith. } case (Zle_lt_or_eq 0 (φ i mod 2)); auto with zarith; intros Hi. 2: generalize H; rewrite <-Hi, Zmult_0_l. 2: replace 0%Z with φ 0; auto. 2: now case eqbP. generalize H; replace (φ i mod 2) with 1%Z; auto with zarith. rewrite Zmult_1_l. intros H1. assert (H2: φ (i << (digits - 1)) <> φ 0). { replace φ 0 with 0%Z; auto with zarith. } now case eqbP. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63