proposition: Lemma merge_float2_prop : stable_expr merge_float2_func.
proof: Proof. assert (forall m e, convert_expr (merge_float2_aux m e) = convert_expr (reFloat2 m e)). intros. unfold merge_float2_aux. generalize (compact_float2_correct m e). now destruct (compact_float2 m e). intros [x|x|x y|x y|o x|o x y|x|x|x|x|x|x|f m x] ; try apply refl_equal ; try exact (H x _). simpl. unfold merge_float2_aux. generalize (compact_float2_correct x 0). rewrite <- (Rmult_1_r (IZR x)). now destruct (compact_float2 x 0). destruct o ; try apply refl_equal. destruct x ; try apply refl_equal. simpl. rewrite H. now rewrite <- Gappa_dyadic.Fopp2_correct. destruct o ; try apply refl_equal. destruct x ; try apply refl_equal. destruct y ; try apply refl_equal. simpl. rewrite H. now rewrite <- Gappa_dyadic.Fmult2_correct. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library