proposition: Lemma le_neg : forall x, ((0 <= x) -> False) <-> 0 < -x.
proof: Proof. intro. rewrite lt_le_iff. split ; intros H. - apply Znot_le_gt in H. apply Zgt_le_succ in H. rewrite le_0_iff in H. ring_simplify in H; auto. - intro H0. assert (C := (Z.add_le_mono _ _ _ _ H H0)). ring_simplify in C. compute in C. apply C ; reflexivity. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac