proposition: Lemma float2_shl_correct : forall m e : Z, forall d : positive, Float2 (shl m d) (e - Zpos d) = Float2 m e :>R.
proof: Proof. intros m e d. replace (shl m d) with (m * Zpower_pos 2 d)%Z. unfold float2R. rewrite (F2R_change_exp _ (e - Zpos d) _ e). simpl. now replace (e - (e - Zpos d))%Z with (Zpos d) by ring. generalize (Zgt_pos_0 d). lia. rewrite Zmult_comm. destruct m as [|m|m] ; simpl. apply Zmult_0_r. now rewrite shift_pos_correct. change (Zneg (shift_pos d m)) with (- Zpos (shift_pos d m))%Z. rewrite shift_pos_correct. now rewrite Zopp_mult_distr_r. Qed.
imports: Coq(ZArith Reals Lia) Flocq(Raux Defs Float_prop Operations) Gappa_definitions