proposition: Lemma asr_land : forall x y, (Uint63.to_Z y <= 62)%Z -> to_Z x = (to_Z (asr x y) * (2 ^ Uint63.to_Z y) + Uint63.to_Z (x land (lsl 1 y - 1)))%Z.
proof: Proof. intros x y Hy. rewrite asr_spec, land_spec', Uint63.sub_spec, lsl_spec. change (Uint63.to_Z 1) with 1%Z. rewrite Z.mul_1_l. rewrite (Z.mod_small (2 ^ _)). 2: { change wB with (2 ^ 63)%Z. split. apply (Zpower_ge_0 radix2). apply (Zpower_lt radix2); lia. } rewrite Z.mod_small. 2: { change wB with (2 ^ 63)%Z. split. apply Z.lt_le_pred. apply (Zpower_gt_0 radix2). apply Uint63.to_Z_bounded. apply Z.lt_pred_le. apply (Zpower_le radix2). lia. } change (2 ^ _ - 1)%Z with (Z.pred (2 ^ Uint63.to_Z y)). rewrite <-Z.ones_equiv. rewrite Z.land_ones by apply Uint63.to_Z_bounded. unfold to_Z at 3. rewrite (proj2 (Uint63.ltb_spec _ _)) by now apply Z.le_lt_trans with (1 := Hy). rewrite <-(to_Z_mod_Uint63to_Z x). rewrite <-Znumtheory.Zmod_div_mod. - rewrite Z.mul_comm. apply Zdiv.Z_div_mod_eq_full. - apply (Zpower_gt_0 radix2). apply Uint63.to_Z_bounded. - easy. - change wB with (2 ^ 63)%Z. replace 63%Z with (63 - Uint63.to_Z y + Uint63.to_Z y)%Z by ring. rewrite Z.pow_add_r. apply Z.divide_factor_r. lia. apply Uint63.to_Z_bounded. Qed.
imports: Coq(Reals Psatz PrimInt63 Uint63 Sint63 PArray Floats) Flocq(Core PrimFloat BinarySingleNaN) Missing.Flocq Xreal Basic Sig Interval Float Float_full Specific_bigint Specific_ops Primitive_ops Lang_expr Lang_tac Interval_helper