proposition: Lemma ring_ops_wd : ring_eq_ext rplus rtimes ropp req.
proof: Proof. constructor. - exact rplus_morph. - exact rtimes_morph. - exact ropp_morph. Qed.
imports: OrderedRing RingMicromega ZArith_base InitialRing Setoid ZArithRing