…lution of an integral equation.
… other way around. SimpleIntegration.v defines integral for uniformly comtinuous functions; AbstractIntegration.v proves properties of integral. Also proved several lemmas about rational numbers.
…ad of c-corn
… required segment
…ag_lip and compose_lip) to avoid requiring MetricSpaceClass when not necessary. Now they require MetricSpaceBall or ExtMetricSpaceClass, which are superclasses of MetricSpaceClass. This way we don't need proving that sigma-types and product types are MetricSpaceClass's. Defined the computational part of Picard operator.