proposition: Lemma CReal_mult_plus_distr_r : forall r1 r2 r3 : CReal, (r2 + r3) * r1 == (r2 * r1) + (r3 * r1).
proof: Proof. intros. rewrite CReal_mult_comm, CReal_mult_plus_distr_l, <- (CReal_mult_comm r1), <- (CReal_mult_comm r1). reflexivity. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra