proposition: Lemma Continuous_I_wd : Feq I F G -> Continuous_I Hab F -> Continuous_I Hab G.
proof: Proof. intros H H0. elim H0; clear H0; intros Hinc H0. elim H; clear H; intros incF' H'. elim H'; clear H'; intros incG' H. split. apply incG'. intros e He; elim (H0 e He); clear H0; intros d H0 H1. exists d. assumption. intros x y H2 H3 Hx Hy H4. apply leEq_wdl with (AbsIR (F x (incF' x H2) [-]F y (incF' y H3))). apply H1; assumption. simpl in H. apply AbsIR_wd. apply cg_minus_wd; apply H; assumption. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac