proposition: Lemma Continuous_I_const : forall c : IR, Continuous_I Hab [-C-]c.
proof: Proof. intro. split. Included. intros; exists OneR. apply pos_one. intros. apply leEq_wdl with (AbsIR [0]). astepl ZeroR; apply less_leEq; assumption. algebra. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac