proposition: Lemma compact_float10_correct : forall m e, float10R (compact_float10 m e) = float10R (Float10 m e).
proof: Proof. unfold float10R, F2R. simpl. intros [|m|m] e ; simpl. now rewrite 2!Rmult_0_l. rewrite <- (float10_of_pos_correct m). destruct (float10_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 <- (float10_of_pos_correct m). destruct (float10_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