proposition: Lemma to_Z_split x : φ x = φ (x >> 1) * 2 + φ (bit x 0).
proof: Proof. case (to_Z_bounded x); intros H1x H2x. case (to_Z_bounded (bit x 0)); intros H1b H2b. assert (F1: 0 <= φ (x >> 1) < wB/2). { rewrite -> lsr_spec, to_Z_1, Z.pow_1_r. split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. } rewrite -> (bit_split x) at 1. rewrite -> add_spec, Zmod_small, lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; split; auto with zarith. - change wB with ((wB/2)*2); auto with zarith. - rewrite -> lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; auto with zarith. change wB with ((wB/2)*2); auto with zarith. - rewrite -> lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; auto with zarith. 2: change wB with ((wB/2)*2); auto with zarith. change wB with (((wB/2 - 1) * 2 + 1) + 1). assert (φ (bit x 0) <= 1); auto with zarith. case bit; discriminate. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63