proposition: Lemma part_int_minus : Feq I (F{-}G) (PartInt (IMinus f g)).
proof: Proof. elim Ff; intros incF Hf. elim Hf; clear Ff Hf; intros incF' Hf. elim Gg; intros incG Hg. elim Hg; clear Gg Hg; intros incG' Hg. apply eq_imp_Feq. Included. Included. intros; simpl in |- *; simpl in Hf, Hg. simpl in |- *; algebra. Qed.
imports: CoRN.ftc.IntervalFunct