proposition: Lemma eq_le_iff : forall x, 0 = x <-> (0 <= x /\ x <= 0).
proof: Proof. intros. split ; intros H. - subst. compute. intuition congruence. - destruct H. apply Z.le_antisymm; auto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac