proposition: Lemma CReal_mult_lt_reg_r : forall r r1 r2, 0 < r -> r1 * r < r2 * r -> r1 < r2.
proof: Proof. intros. apply CReal_mult_lt_reg_l with r. - exact H. - now rewrite 2!(CReal_mult_comm r). Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra