proposition: Lemma interval_restriction : forall lb ub a b, interval lb ub a -> interval lb ub b -> included (interval a b) (interval lb ub).
proof: Proof. intros lb ub a b a_in b_in x x_in ; split. transitivity a ; [apply a_in | apply x_in]. transitivity b ; [apply x_in | apply b_in]. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics