proposition: Lemma scal_R_Cmult : forall (x : R) (y : C), scal (V := C_R_ModuleSpace) x y = Cmult x y.
proof: Proof. intros x y. apply injective_projections ; rewrite /scal /= /scal /= /mult /= ; ring. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy