fact: Definition Fplus_naive sx mx ex sy my ey ez := (Zplus (cond_Zopp sx (Zpos (fst (shl_align mx ex ez)))) (cond_Zopp sy (Zpos (fst (shl_align my ey ez))))).
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative