proposition: Lemma Diffble_div : bnd_away_zero_in_P G I -> Diffble I pI (F{/}G).
proof: Proof. intro. apply Diffble_wd with (F{*}{1/}G). apply eq_imp_Feq. apply included_FMult. apply Diffble_imp_inc with pI; apply diffF. apply included_FRecip. apply Diffble_imp_inc with pI; apply diffG. Included. apply included_FDiv. apply Diffble_imp_inc with pI; apply diffF. apply Diffble_imp_inc with pI; apply diffG. Included. intros; simpl in |- *; rational. apply Diffble_mult; auto. apply Diffble_recip; auto. Qed.
imports: CoRN.ftc.MoreIntervals