proposition: Lemma proper_compact_in_interval : forall I pI x Hx, proper (compact_in_interval I pI x Hx).
proof: Proof. intro. elim I; simpl in |- *; intros; try inversion_clear Hx. apply less_plusOne. apply less_plusOne. apply shift_minus_less; apply less_plusOne. apply less_plusOne. apply shift_minus_less; apply less_plusOne. eapply less_transitive_unfolded; [ apply cip1'' | apply cip1'''' ]; auto. eapply less_leEq_trans; [ apply cip1'' | apply cip1''' ]; auto. eapply leEq_less_trans; [ apply cip1' | apply cip1'''' ]; auto. auto. Qed.
imports: CoRN.ftc.NthDerivative