proposition: Lemma RtoC_mult (x y : R) : RtoC (x * y) = RtoC x * RtoC y.
proof: Proof. unfold RtoC, Cmult ; simpl. apply injective_projections ; simpl ; ring. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy