proposition: Lemma Diffble_recip : bnd_away_zero_in_P G I -> Diffble I pI {1/}G.
proof: Proof. elim diffG; intros incG diffbleG Gbnd. cut (forall x : IR, I x -> forall Hx, Part G x Hx [#] [0]); intros. split. Included. intros; apply Diffble_I_recip; auto. Included. Qed.
imports: CoRN.ftc.MoreIntervals