proposition: Lemma Continuous_I_minus : Continuous_I Hab (F{-}G).
proof: Proof. apply Continuous_I_wd with (F{+}{--}G). FEQ. apply Continuous_I_plus. apply contF. apply Continuous_I_inv; apply contG. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac