proposition: Lemma CRopp_gt_lt_contravar : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R), r2 < r1 -> - r1 < - r2.
proof: Proof. intros. apply (CRplus_lt_reg_l R r1). destruct (CRisRing R). apply (CRle_lt_trans _ 0). - apply Ropp_def. - apply (CRplus_lt_compat_l R (CRopp R r2)) in H. apply (CRle_lt_trans _ (CRplus R (CRopp R r2) r2)). + apply (CRle_trans _ (CRplus R r2 (CRopp R r2))). * destruct (Ropp_def r2). exact H0. * destruct (Radd_comm r2 (CRopp R r2)). exact H1. + apply (CRlt_le_trans _ _ _ H). destruct (Radd_comm r1 (CRopp R r2)). exact H0. Qed.
imports: QArith Qabs Qround