Definition M10 := Fnum x10.
Hypothesis M10_bound : 1 <= M10 <= 10 ^ 16 - 1.
Definition e10 := Fexp x10 + 15.
Hypothesis e10_bound : -383 <= e10 <= 384.