proposition: Lemma Dminus : forall (D:C -> Prop) (df dg f g:C -> C) (x0:C), D_in f df D x0 -> D_in g dg D x0 -> D_in (fun x:C => f x - g x) (fun x:C => df x - dg x) D x0.
proof: Proof. unfold Rminus in |- *; intros; generalize (Dopp D g dg x0 H0); intro; apply (Dadd D df (fun x:C => - dg x) f (fun x:C => - g x) x0); assumption. Qed.
imports: Ctacfield Cnorm Cprop_base Classical_Prop Classical_Pred_Type Cmet