proposition: Lemma Qeval_op2_hold : forall k op q1 q2, Tauto.hold k (Qeval_op2 k op q1 q2) <-> Qeval_pop2 op q1 q2.
proof: Proof. destruct k. - simpl ; tauto. - simpl. apply pop2_bop2. Qed.
imports: OrderedRing RingMicromega Refl QArith Qfield EnvRing