proposition: Lemma eq_cnf : forall x, (0 <= x - 1 -> False) /\ (0 <= -1 - x -> False) <-> x = 0.
proof: Proof. intros x. rewrite Z.eq_sym_iff. rewrite eq_le_iff. rewrite (le_0_iff x 0). rewrite !le_neg. rewrite !lt_le_iff. replace (- (x - 1) -1) with (-x) by ring. replace (- (-1 - x) -1) with x by ring. split ; intros (H1 & H2); auto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac