proposition: Lemma Fsub_split : forall beta mode prec (x y : float beta), FtoX (Fsub mode prec x y) = (FtoX (Fadd mode prec x (Fneg y))).
proof: Proof. intros. unfold Fneg, Fadd, Fsub, Fadd_slow, Fsub_slow. case y ; trivial. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic