proposition: Lemma neighbourhood_P1 : forall (D1 D2:R -> Prop) (x:R), included D1 D2 -> neighbourhood D1 x -> neighbourhood D2 x.
proof: Proof. unfold included, neighbourhood; intros; elim H0; intros; exists x0; intros; unfold included; unfold included in H1; intros; apply (H _ (H1 _ H2)). Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type