proposition: Lemma Reval_op2_hold : forall b op q1 q2, Tauto.hold b (Reval_op2 b op q1 q2) <-> Reval_pop2 op q1 q2.
proof: Proof. destruct b. - simpl ; tauto. - simpl. apply pop2_bop2. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant EnvRing