proposition: Theorem Fadd_slow_correct : forall beta mode prec (x y : float beta), FtoX (Fadd_slow mode prec x y) = Xround beta mode prec (Xadd (FtoX x) (FtoX y)).
proof: Proof. intros beta mode prec x y. unfold Fadd_slow. rewrite Fround_at_prec_pos_Eq. now rewrite Fadd_slow_aux_correct. apply UtoX_pos_Eq. rewrite Fadd_slow_aux_correct. destruct x as [| |sx mx ex]. easy. now case y. now case y. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic