proposition: Lemma le_0_iff : forall x y, x <= y <-> 0 <= y - x.
proof: Proof. split ; intros. - apply Zle_minus_le_0; auto. - apply Zle_0_minus_le; auto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac