proposition: Lemma CRmult_lt_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), 0 < r -> r * r1 < r * r2 -> r1 < r2.
proof: Proof. intros. rewrite (Rmul_comm (CRisRing R) r r1) in H0. rewrite (Rmul_comm (CRisRing R) r r2) in H0. apply CRmult_lt_reg_r in H0. - exact H0. - exact H. Qed.
imports: QArith Qabs Qround