proposition: Lemma Continuous_recip : bnd_away_zero_in_P G I -> Continuous I {1/}G.
proof: Proof. intro H. elim contG; intros incG' contG'. cut (forall x : IR, I x -> forall Hx, G x Hx [#] [0]). intro H0. split; Contin. intros x H0 Hx. apply bnd_imp_ap_zero with (Compact (leEq_reflexive _ x)); auto. apply H; auto. exact (compact_single_iprop I x H0). exact (compact_single_prop x). Qed.
imports: CoRN.ftc.MoreIntervals