proposition: Lemma CReal_mult_lt_compat_r : forall x y z : CReal, 0 < x -> y < z -> y*x < z*x.
proof: Proof. intros. rewrite <- (CReal_mult_comm x), <- (CReal_mult_comm x). apply (CReal_mult_lt_compat_l x); assumption. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra