proposition: Lemma nonvoid_char : forall (I : interval) (x : IR), I x -> nonvoid I.
proof: Proof. intro; induction I; simpl in |- *; intros x H; auto; inversion_clear H. apply less_transitive_unfolded with x; auto. apply less_leEq_trans with x; auto. apply leEq_less_trans with x; auto. apply leEq_transitive with x; auto. Qed.
imports: CoRN.ftc.NthDerivative