fact: Definition Fplus (x y : float) := Float (Fnum x * Zpower_nat radix (Z.abs_nat (Fexp x - Z.min (Fexp x) (Fexp y))) + Fnum y * Zpower_nat radix (Z.abs_nat (Fexp y - Z.min (Fexp x) (Fexp y)))) (Z.min (Fexp x) (Fexp y)).
imports: Reals ZArith List PeanoNat Psatz