proposition: Lemma pop2_bop2 : forall (op : Op2) (q1 q2 : Q), is_true (Qeval_bop2 op q1 q2) <-> Qeval_pop2 op q1 q2.
proof: Proof. unfold is_true. destruct op ; simpl; intros. - apply Qeq_bool_iff. - rewrite <- Qeq_bool_iff. rewrite negb_true_iff. destruct (Qeq_bool q1 q2) ; intuition congruence. - apply Qle_bool_iff. - apply Qle_bool_iff. - apply Qlt_bool_iff. - apply Qlt_bool_iff. Qed.
imports: OrderedRing RingMicromega Refl QArith Qfield EnvRing