proposition: Lemma Zeval_op2_hold : forall k op q1 q2, Tauto.hold k (Zeval_op2 k op q1 q2) <-> Zeval_pop2 op q1 q2.
proof: Proof. intro k; destruct k. - simpl ; tauto. - simpl. apply pop2_bop2. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing