proposition: Lemma Continuous_NRoot : forall n H, (forall x : IR, I x -> forall Hx, [0][<=]F x Hx) -> Continuous I (FNRoot F n H).
proof: Proof. intros n H. elim contF; intros incF' contF'. split; Contin. Qed.
imports: CoRN.ftc.MoreIntervals