proposition: Lemma pop2_bop2 : forall (op : Op2) (q1 q2 : Z), is_true (Zeval_bop2 op q1 q2) <-> Zeval_pop2 op q1 q2.
proof: Proof. unfold is_true. intro op; destruct op ; simpl; intros q1 q2. - apply Z.eqb_eq. - rewrite <- Z.eqb_eq. rewrite negb_true_iff. destruct (q1 =? q2) ; intuition congruence. - apply Z.leb_le. - rewrite Z.geb_le. rewrite Z.ge_le_iff. tauto. - apply Z.ltb_lt. - rewrite <- Zgt_is_gt_bool; tauto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing