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