proposition: Lemma Continuous_I_div : Continuous_I Hab (F{/}G).
proof: Proof. apply Continuous_I_wd with (F{*}{1/}G). FEQ. apply Continuous_I_mult. assumption. apply Continuous_I_recip; assumption. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac