proposition: Lemma compact_posfloat10_correct : forall m e, convert_expr (compact_posfloat10 m e) = (IZR m * bpow radix10 e)%R.
proof: Proof. intros m e. unfold compact_posfloat10. generalize (compact_float10_correct m e). destruct compact_float10 as [m' e']. destruct e'. unfold float10R, F2R. simpl. now rewrite Rmult_1_r. destruct m' as [|m'|m'] ; try easy. simpl. unfold float10R, F2R. simpl. now rewrite Ropp_mult_distr_l. destruct m' as [|m'|m'] ; try easy. simpl. unfold float10R, F2R. simpl. now rewrite Ropp_mult_distr_l. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library