proposition: Lemma inject_Q_product (l: list Q) : (' cr_Product l) == @cr_Product CRasCRing (map inject_Q_CR l).
proof: Proof. induction l. reflexivity. change (' (a * cr_Product l)%Q == @cr_Product CRasCRing (map inject_Q_CR (a :: l))). rewrite <- CRmult_Qmult. rewrite IHl. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.model.reals.CRreal CoRN.metric2.Complete CoRN.reals.fast.CRFieldOps CoRN.model.rings.Qring CoRN.algebra.CRing_Homomorphisms CoRN.model.metric2.Qmetric CoRN.tactics.CornTac CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders CRArith