fact: Fixpoint XpowM (X : MetricSpace) (m : nat) {struct m} : MetricSpace := match m with | 0 => X | 1 => X | S n => ProductMS X (XpowM X n) end.
imports: ssreflect CSetoids CSetoidFun CFields CPolynomials Program Omega Equivalence Morphisms Wf Morphisms CRings CRing_Homomorphisms Rational Setoid CPoly_NthCoeff CPoly_Degree CReals Intervals CauchySeq IntervalFunct MoreIntervals MoreFunctions Composition seq bigopsClass Structures ProductMetric CRIR Integration Qmetric QposMinMax