fact: Fixpoint Picard_seq (n : nat) : Q --> CR := match n with | O => f ∘ Cunit | S m => (Picard (Picard_seq m) )∘ Cunit end.
imports: CRtrans Qmetric ProductMetric CompleteProduct Unicode.Utf8 CPoly_Newton metric2.Classified Circle AbstractIntegration SimpleIntegration