proposition: Lemma CRmult_plus_distr_l : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier R), r1 * (r2 + r3) == (r1 * r2) + (r1 * r3).
proof: Proof. intros. destruct (CRisRing R). transitivity ((r2 + r3) * r1). - apply Rmul_comm. - transitivity ((r2 * r1) + (r3 * r1)). + apply Rdistr_l. + transitivity ((r1 * r2) + (r3 * r1)). * destruct (CRisRingExt R). apply Radd_ext. -- apply Rmul_comm. -- apply CReq_refl. * destruct (CRisRingExt R). apply Radd_ext. -- apply CReq_refl. -- apply Rmul_comm. Qed.
imports: QArith Qabs Qround