proposition: Lemma Zsor : SOR 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt.
proof: Proof. constructor ; intros ; subst; try reflexivity. - apply Zsth. - apply Zth. - auto using Z.le_antisymm. - eauto using Z.le_trans. - apply Z.le_neq. - apply Z.lt_trichotomy. - apply Z.add_le_mono_l; assumption. - apply Z.mul_pos_pos ; auto. - discriminate. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing