proposition: Lemma mult_real_fct_0: forall f, mult_real_fct 0 f == (fun _ => 0).
proof: Proof. intros f x ; unfold mult_real_fct ; apply Rmult_0_l. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra