proposition: Lemma is_linear_RtoC : is_linear RtoC.
proof: Proof. split => //=. by intros ; rewrite RtoC_plus. intros ; rewrite {2}/scal /= /prod_scal /= scal_zero_r. reflexivity. exists (sqrt 2) ; split. apply Rlt_sqrt2_0. intros. eapply Rle_trans. rewrite -Cmod_norm. apply Cmod_2Rmax. simpl. rewrite Rabs_R0. rewrite Rmax_left. apply Rle_refl. apply Rabs_pos. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)