proposition: Lemma Dminus : forall (D:R -> Prop) (df dg f g:R -> R) (x0:R), D_in f df D x0 -> D_in g dg D x0 -> D_in (fun x:R => f x - g x) (fun x:R => df x - dg x) D x0.
proof: Proof. unfold Rminus; intros; generalize (Dopp D g dg x0 H0); intro; apply (Dadd D df (fun x:R => - dg x) f (fun x:R => - g x) x0); assumption. Qed.
imports: Rbase Rfunctions Rlimit Lra Lia