proposition: Lemma Zring_morph : ring_morph 0 1 rplus rtimes rminus ropp req 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool gen_order_phi_Z.
proof: Proof. exact (gen_phiZ_morph (SORsetoid sor) ring_ops_wd (SORrt sor)). Qed.
imports: OrderedRing RingMicromega ZArith_base InitialRing Setoid ZArithRing