proposition: Lemma compact_float2_correct : forall m e, float2R (compact_float2 m e) = float2R (Float2 m e).
proof: Proof. unfold float2R, F2R. simpl. intros [|m|m] e ; simpl. now rewrite 2!Rmult_0_l. rewrite <- (float2_of_pos_correct m). destruct (float2_of_pos m) as (m1, e1). simpl. rewrite Zplus_comm. now rewrite bpow_plus, <- Rmult_assoc. change (IZR (Zneg m)) with (- IZR (Zpos m))%R. rewrite <- (float2_of_pos_correct m). destruct (float2_of_pos m) as (m1, e1). simpl. rewrite Zplus_comm. rewrite bpow_plus, <- Rmult_assoc. now rewrite opp_IZR, Ropp_mult_distr_l_reverse. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library