proposition: Lemma included_trans : forall D1 D2 D3:R -> Prop, included D1 D2 -> included D2 D3 -> included D1 D3.
proof: Proof. unfold included; intros; apply H0; apply H; apply H1. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type