proposition: Lemma Picard_uc: (is_UniformlyContinuousFunction Picard_raw (fun e => e)%Qpos).
proof: Proof. admit. Qed.
imports: CRtrans Qmetric ProductMetric CompleteProduct Unicode.Utf8 CPoly_Newton metric2.Classified Circle AbstractIntegration SimpleIntegration