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