proposition: Theorem Fadd_slow_aux_correct : forall beta (x y : float beta), UtoX (Fadd_slow_aux x y) = Xadd (FtoX x) (FtoX y).
proof: Proof. intros. case x. case y ; intros ; apply refl_equal. simpl. case y. apply refl_equal. unfold FtoX. rewrite Rplus_0_l. apply refl_equal. intros sy my ey. unfold FtoX. rewrite Rplus_0_l. apply refl_equal. intros sx mx ex. simpl. case y. apply refl_equal. unfold FtoX. rewrite Rplus_0_r. apply refl_equal. intros sy my ey. rewrite Fadd_slow_aux2_correct. apply refl_equal. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic