fact: Definition Fshift2 (x y : float2) := match (Fexp x - Fexp y)%Z with | Zpos p => (shl (Fnum x) p, Fnum y, Fexp y) | Zneg p => (Fnum x, shl (Fnum y) p, Fexp x) | Z0 => (Fnum x, Fnum y, Fexp x) end.
imports: Coq(ZArith Reals Lia) Flocq(Raux Defs Float_prop Operations) Gappa_definitions