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