proposition: Lemma Dmult_const : forall (D:R -> Prop) (f df:R -> R) (x0 a:R), D_in f df D x0 -> D_in (fun x:R => a * f x) (fun x:R => a * df x) D x0.
proof: Proof. intros; generalize (Dmult D (fun _:R => 0) df (fun _:R => a) f x0 (Dconst D a x0) H); unfold D_in; intros; rewrite (Rmult_0_l (f x0)) in H0; rewrite (let (H1, H2) := Rplus_ne (a * df x0) in H2) in H0; assumption. Qed.
imports: Rbase Rfunctions Rlimit Lra Lia