proposition: Lemma req_trans : forall x y z, req x y -> req y z -> req x z.
proof: Proof. destruct (SORsetoid sor) as (_,_,Equivalence_Transitive). apply Equivalence_Transitive. Qed.
imports: OrderedRing RingMicromega ZArith_base InitialRing Setoid ZArithRing