proposition: Lemma part_int_div : Feq I (F{/}G) (PartInt (IDiv f g Hg)).
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 Hf, Hg'; simpl in |- *. algebra. Qed.
imports: CoRN.ftc.IntervalFunct