proposition: Lemma lt_le_iff : forall x, 0 < x <-> 0 <= x - 1.
proof: Proof. split ; intros H. - apply Zlt_succ_le. ring_simplify. auto. - apply Zle_lt_succ in H. ring_simplify in H. auto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac