proposition: Lemma iprop_compact_in_interval : forall I pI x Hx, compact_in_interval I pI x Hx x.
proof: Proof. intro. elim I; simpl in |- *; intros; try inversion_clear Hx; split; auto; try apply leEq_reflexive. apply less_leEq; apply less_plusOne. apply less_leEq; apply less_plusOne. apply less_leEq; apply shift_minus_less; apply less_plusOne. apply less_leEq; apply less_plusOne. apply less_leEq; apply shift_minus_less; apply less_plusOne. apply less_leEq; apply cip1''; auto. apply less_leEq; apply cip1''''; auto. apply less_leEq; apply cip1''; auto. apply less_leEq; apply cip1''''; auto. Qed.
imports: CoRN.ftc.NthDerivative