proposition: Lemma is_linear_C_R (l : C -> C) : is_linear (U := C_NormedModule) (V := C_NormedModule) l -> is_linear (U := C_R_NormedModule) (V := C_R_NormedModule) l.
proof: Proof. intros Lf. - split. intros ; apply Lf. simpl ; intros. rewrite !scal_R_Cmult ; by apply Lf. case: Lf => _ _ [M Lf]. exists M ; split. by apply Lf. intros. rewrite -!Cmod_norm. apply Lf. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)