proposition: Lemma proper_compact_in_interval2' : forall I pI x y Hx Hy H, Lend (I:=compact_in_interval2 I pI x y Hx Hy) H [<] Rend (I:=compact_in_interval2 I pI x y Hx Hy) H.
proof: Proof. do 6 intro. cut (proper (compact_in_interval2 I pI x y Hx Hy)). 2: apply proper_compact_in_interval2. elim (compact_in_interval2 I pI x y Hx Hy); intros; try inversion H. simpl in |- *; simpl in H; auto. Qed.
imports: CoRN.ftc.NthDerivative