proposition: Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq Qle Qlt.
proof: Proof. constructor; intros ; subst ; try (intuition (subst; auto with qarith)). - apply Q_Setoid. - rewrite H ; rewrite H0 ; reflexivity. - rewrite H ; rewrite H0 ; reflexivity. - rewrite H ; auto ; reflexivity. - rewrite <- H ; rewrite <- H0 ; auto. - rewrite H ; rewrite H0 ; auto. - rewrite <- H ; rewrite <- H0 ; auto. - rewrite H ; rewrite H0 ; auto. - apply Qsrt. - eapply Qle_trans ; eauto. - apply (Qlt_not_eq n m H H0) ; auto. - destruct(Q_dec n m) as [[H1 |H1] | H1 ] ; tauto. - apply (Qplus_le_compat p p n m (Qle_refl p) H). - generalize (Qmult_lt_compat_r 0 n m H0 H). rewrite Qmult_0_l. auto. - compute in H. discriminate. Qed.
imports: OrderedRing RingMicromega Refl QArith Qfield