proposition: Lemma Continuous_I_scal : forall c : IR, Continuous_I Hab (c{**}F).
proof: Proof. intros. unfold Fscalmult in |- *. apply Continuous_I_mult. apply Continuous_I_const. apply contF. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac