proposition: Lemma Dmult_const : forall (D:C -> Prop) (f df:C -> C) (x0 a:C), D_in f df D x0 -> D_in (fun x:C => a * f x) (fun x:C => a * df x) D x0.
proof: Proof. intros; generalize (Dmult D (fun _:C => C0) df (fun _:C => a) f x0 (Dconst D a x0) H); unfold D_in in |- *; intros; rewrite (Cmult_0_l (f x0)) in H0. rewrite Cadd_0_l in H0. assumption. Qed.
imports: Ctacfield Cnorm Cprop_base Classical_Prop Classical_Pred_Type Cmet