proposition: Lemma compact_posfloat2_correct : forall m e, convert_expr (compact_posfloat2 m e) = (IZR m * bpow radix2 e)%R.
proof: Proof. intros m e. unfold compact_posfloat2. generalize (compact_float2_correct m e). destruct compact_float2 as [m' e']. destruct e'. unfold float2R, F2R. simpl. now rewrite Rmult_1_r. destruct m' as [|m'|m'] ; try easy. simpl. now rewrite <- Gappa_dyadic.Fopp2_correct. destruct m' as [|m'|m'] ; try easy. simpl. now rewrite <- Gappa_dyadic.Fopp2_correct. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library