proposition: Lemma shiftr_pos p : let d := Z.log2 (Z.pos p) in let s := Z.shiftr (Z.pos p) (d - 52) in (0 <= d - 52 -> (s * 2 ^ (d - 52) <= Z.pos p < (s + 1) * 2 ^ (d - 52) /\ s < 2^53))%Z.
proof: Proof. intros d s. unfold s. unfold d. clear d s; intro He. rewrite (Z.shiftr_div_pow2 _ _ He). split; [split| ]. { now rewrite Zmult_comm; apply Z_mult_div_ge, pow2_pos. } { set (a := Z.pos p). set (b := (2^_)%Z). rewrite Z.mul_add_distr_r, Z.mul_1_l, Z.mul_comm. rewrite (Z_div_mod_eq a b) at 1; [ |now apply pow2_pos]. now apply Zplus_lt_compat_l, Z_mod_lt, pow2_pos. } apply (Zmult_gt_0_lt_reg_r _ _ _ (pow2_pos _ He)). rewrite Z.mul_comm. apply (Z.le_lt_trans _ _ _ (Z_mult_div_ge _ _ (pow2_pos _ He))). rewrite <-Z.pow_add_r; [ |lia|exact He]. replace (_ + _)%Z with (Z.log2 (Z.pos p) + 1)%Z by ring. now apply Z.log2_spec. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig