proposition: Theorem Fsub_correct : forall beta mode prec (x y : float beta), FtoX (Fsub mode prec x y) = Xround beta mode prec (Xsub (FtoX x) (FtoX y)).
proof: Proof. intros. rewrite Fsub_split. rewrite Xsub_split. rewrite <- Fneg_correct. apply Fadd_correct. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic