proposition: Lemma CRmult_lt_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), 0 < r -> r1 * r < r2 * r -> r1 < r2.
proof: Proof. intros. apply (CRmult_lt_compat_r ((/ r) (inr H))) in H0. 2: apply CRinv_0_lt_compat, H. apply (CRle_lt_trans _ ((r1 * r) * ((/ r) (inr H)))). - clear H0. apply (CRle_trans _ (CRmult R r1 1)). + destruct (CRmult_1_r r1). exact H0. + apply (CRle_trans _ (CRmult R r1 (CRmult R r ((/ r) (inr H))))). * destruct (Rmul_ext (CRisRingExt R) r1 r1 (CReq_refl r1) (r * ((/ r) (inr H))) 1). -- apply CRinv_r. -- exact H0. * destruct (Rmul_assoc (CRisRing R) r1 r ((/ r) (inr H))). exact H1. - apply (CRlt_le_trans _ ((r2 * r) * ((/ r) (inr H)))). { exact H0. } clear H0. apply (CRle_trans _ (r2 * 1)). 2: destruct (CRmult_1_r r2); exact H1. apply (CRle_trans _ (r2 * (r * ((/ r) (inr H))))). { destruct (Rmul_assoc (CRisRing R) r2 r ((/ r) (inr H))). exact H0. } destruct (Rmul_ext (CRisRingExt R) r2 r2 (CReq_refl r2) (r * ((/ r) (inr H))) 1). + apply CRinv_r. + exact H1. Qed.
imports: QArith Qabs Qround