proposition: Lemma part_int_recip : Feq I {1/}G (PartInt (IRecip g Hg)).
proof: Proof. elim Gg; intros incG Hg'. elim Hg'; clear Gg Hg'; intros incG' Hg'. apply eq_imp_Feq. Included. Included. intros; simpl in Hg'; simpl in |- *; algebra. Qed.
imports: CoRN.ftc.IntervalFunct