proposition: Lemma to_Z_branch_bit : forall k m (SMALL : (m <? 63 = true)%uint63), to_Z ((k >> (m + 1)) << (m + 1) + 1 << m)%uint63 = ((to_Z k / 2^ (to_Z m + 1)) * 2^ (to_Z m + 1) + 2^ (to_Z m))%Z.
proof: Proof. intros. rewrite add_spec. rewrite! lsl_spec. rewrite lsr_spec. rewrite add_spec. change (to_Z m + to_Z 1%uint63)%Z with (to_Z m + 1)%Z. assert (B1 : (0 <= φ (1)%uint63 * 2 ^ φ (m)%uint63 < wB)%Z). { replace (φ (1)%uint63 * 2 ^ φ (m)%uint63)%Z with (2 ^ to_Z m)%Z by lia. split. apply Z.pow_nonneg. lia. apply Z.pow_lt_mono_r. lia. lia. lia. } assert (B2 : (2^1 <= 2 ^ ((φ (m)%uint63 + 1)))%Z). { apply Z.pow_le_mono_r. lia. lia. } assert (B3 : (0 <= φ (k)%uint63 / 2 ^ ((φ (m)%uint63 + 1)))%Z). { nia. } assert (B4 : (0 <= φ (k)%uint63 / 2 ^ ((φ (m)%uint63 + 1) mod wB) * 2 ^ ((φ (m)%uint63 + 1) mod wB) < wB)%Z). { change (Z.of_nat size) with 63%Z in *. rewrite Z.mod_small by lia. split. apply Z.mul_nonneg_nonneg ; nia. nia. } rewrite! Z.mod_small; auto. - lia. - unfold wB. change (Z.of_nat size) with 63%Z. lia. - rewrite Z.mod_small;auto. rewrite Z.mod_small;auto. rewrite Z.mod_small;auto. split. lia. clear B4. unfold wB in *. change (Z.of_nat size) with 63%Z. assert (φ (k)%uint63 / 2 ^ (φ (m)%uint63 + 1) * 2 ^ (φ (m)%uint63 + 1) = to_Z k - to_Z k mod 2 ^ (φ (m)%uint63 + 1))%Z. nia. rewrite H. change (to_Z 1%uint63) with 1%Z. rewrite Z.mul_1_l. apply sub_pow2. lia. lia. unfold wB. change (Z.of_nat size) with 63%Z. lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR