proposition: Lemma Rsor : SOR R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle Rlt.
proof: Proof. constructor; intros ; subst ; try (intuition (subst; try ring ; auto with real)). - constructor. + constructor. + unfold RelationClasses.Symmetric. auto. + unfold RelationClasses.Transitive. intros. subst. reflexivity. - apply Rsrt. - eapply Rle_trans ; eauto. - apply (Rlt_irrefl m) ; auto. - apply Rnot_le_lt. auto with real. - destruct (total_order_T n m) as [ [H1 | H1] | H1] ; auto. - now apply Rmult_lt_0_compat. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant