Theorem easycomp_correct:
  (easycomp = Lt -> F2R x2 < F2R x10) /\
  (easycomp = Gt -> F2R x2 > F2R x10) /\
  (easycomp = Eq <-> g = phi h).