proposition: Lemma Reval_pop2_eval_op2 : forall o e1 e2, Reval_pop2 o e1 e2 <-> eval_op2 eq Rle Rlt o e1 e2.
proof: Proof. destruct o ; simpl ; try tauto. split. - apply Rge_le. - apply Rle_ge. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant EnvRing