proposition: Lemma continuous_C_id_1 (x : C) : continuous (T := C_UniformSpace) (U := AbsRing_UniformSpace C_AbsRing) (fun y => y) x.
proof: Proof. intros P HP. by apply locally_C. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)