proposition: Lemma part_int_inv : Feq I {--}F (PartInt (IInv f)).
proof: Proof. 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. simpl in |- *; algebra. Qed.
imports: CoRN.ftc.IntervalFunct