proposition: Lemma nonvoid_point : forall I : interval, nonvoid I -> {x : IR | I x}.
proof: Proof. intro. destruct I as [| c| c| c| c| c c0| c c0| c c0| c c0]; simpl in |- *; intros; try rename X into H. exists ZeroR; auto. exists (c[+][1]); apply less_plusOne. exists (c[-][1]); apply shift_minus_less; apply less_plusOne. exists c; apply leEq_reflexive. exists c; apply leEq_reflexive. exists (c[+] (c0[-]c) [/]TwoNZ); split. astepl (c[+][0]); apply plus_resp_less_lft. apply div_resp_pos. apply pos_two. apply shift_less_minus; astepl c; auto. rstepr (c[+] (c0[-]c)). apply plus_resp_less_lft. apply pos_div_two'. apply shift_less_minus; astepl c; auto. exists c0; split; auto; apply leEq_reflexive. exists c; split; auto; apply leEq_reflexive. exists c; split; [ apply leEq_reflexive | auto ]. Qed.
imports: CoRN.ftc.NthDerivative