proposition: Lemma CRmult_plus_distr_r : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier R), (r2 + r3) * r1 == (r2 * r1) + (r3 * r1).
proof: Proof. intros. do 3 rewrite <- (CRmult_comm r1). apply CRmult_plus_distr_l. Qed.
imports: QArith Qabs Qround