proposition: Theorem Fadd_exact_correct : forall beta (x y : float beta), FtoX (Fadd_exact x y) = Xadd (FtoX x) (FtoX y).
proof: Proof. intros. unfold Fadd_exact. rewrite <- (Fadd_slow_aux_correct _ x y). case (Fadd_slow_aux x y) ; simpl ; try apply refl_equal. intros. case p0 ; apply refl_equal. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic