Definition M2 := Fnum x2.
Hypothesis M2_bound : 2 ^ 52 <= M2 <= 2 ^ 53 - 1.
Definition e2 := Fexp x2 + 52.
Hypothesis e2_bound : -1074 <= e2 <= 1023.