proposition: Lemma part_int_nth : forall n : nat, Feq I (F{^}n) (PartInt (INth f n)).
proof: Proof. intro. elim Ff; intros incF Hf. elim Hf; clear Ff Hf; intros incF' Hf. apply eq_imp_Feq. Included. Included. intros; simpl in |- *; simpl in Hf. astepl (Part F x Hx[^]n); astepr (f (Build_subcsetoid_crr IR _ x Hx')[^]n). apply nexp_wd; algebra. Qed.
imports: CoRN.ftc.IntervalFunct