Theorem direct_method_alg_correct :
 ((direct_method_alg = Lt <-> F2R x2 < F2R x10) /\
  (direct_method_alg = Eq <-> F2R x2 = F2R x10) /\
  (direct_method_alg = Gt <-> F2R x2 > F2R x10))%R.