proposition: Lemma Continuous_I_NRoot : forall n Hn, (forall x Hx, I x -> [0][<=]F x Hx) -> Continuous_I Hab (FNRoot F n Hn).
proof: Proof. intros n Hn H. split. Included. intros e He. destruct contF as [contF'' contF']. destruct (contF' (e[^]n)) as [d Hd H0]; clear contF contF'. apply nexp_resp_pos; assumption. exists d. assumption. intros x y Hx0 Hy0 Hx Hy Hxy. set (x':=FNRoot F n Hn x Hx). set (y':=FNRoot F n Hn y Hy). stepl (Max x' y'[-]Min x' y'); [|apply eq_symmetric;apply Abs_Max]. apply shift_minus_leEq. apply power_cancel_leEq with n; try assumption. apply plus_resp_nonneg. apply less_leEq; assumption. apply leEq_Min; apply: NRoot_nonneg. apply leEq_transitive with (e[^]n[+]Min x' y'[^]n). apply shift_leEq_plus. set (Hx':=(ProjT1 (ext2_a IR (Dom F) (fun (x0 : IR) (Hx1 : Dom F x0) => [0][<=]F x0 Hx1) x Hx))). set (Hy':=(ProjT1 (ext2_a IR (Dom F) (fun (x0 : IR) (Hx1 : Dom F x0) => [0][<=]F x0 Hx1) y Hy))). stepl (AbsIR (F x Hx'[-]F y Hy')). apply H0; try assumption. stepr (AbsIR (x'[^]n[-]y'[^]n)). apply AbsIR_wd. apply: bin_op_wd_unfolded; apply eq_symmetric; try apply un_op_wd_unfolded; apply: NRoot_power. csetoid_rewrite (Abs_Max (x'[^]n) (y'[^]n)). apply: bin_op_wd_unfolded; try apply un_op_wd_unfolded. change (Max ((FId{^}n) x' True_constr) ((FId{^}n) y' True_constr)[=]((FId{^}n) (Max x' y') True_constr)). apply Max_monotone. simpl; intros r s _ _ X0 X1 X2. apply: nexp_resp_leEq; try assumption. eapply leEq_transitive;[|apply X0]. apply leEq_Min; apply: NRoot_nonneg. change (Min ((FId{^}n) x' True_constr) ((FId{^}n) y' True_constr)[=]((FId{^}n) (Min x' y') True_constr)). apply Min_monotone. simpl; intros r s _ _ X0 X1 X2. apply: nexp_resp_leEq; try assumption. eapply leEq_transitive;[|apply X0]. apply leEq_Min; apply: NRoot_nonneg. apply power_plus_leEq; try assumption. apply less_leEq; assumption. apply leEq_Min; apply: NRoot_nonneg. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac