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
.