proposition: Lemma Zunsat_sound : forall f, Zunsat f = true -> forall env, eval_nformula env f -> False.
proof: Proof. unfold Zunsat. intros f H env ?. destruct f. eapply check_inconsistent_sound with (1 := Zsor) (2 := ZSORaddon) in H; eauto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing