proposition: Lemma is_linear_C_id_2 : is_linear (U := AbsRing_NormedModule C_AbsRing) (V := C_NormedModule) (fun y : C_NormedModule => y).
proof: Proof. split => //. exists 1 ; split. by apply Rlt_0_1. intros x ; apply Req_le. rewrite Rmult_1_l ; reflexivity. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)