proposition: Lemma cvgeD f g a b : a +? b -> f @ F --> a -> g @ F --> b -> f \+ g @ F --> a + b.
proof: Proof. have yE u v x : u @ F --> +oo -> v @ F --> x%:E -> u \+ v @ F --> +oo. move=> /cvgeyPge/= foo /fine_cvgP[Fg gb]; apply/cvgeyPgey. near=> A; near=> n; have /(_ _)/wrap[//|Fgn] := near Fg n. rewrite -lee_subl_addr// (@le_trans _ _ (A - (x - 1))%:E)//; last by near: n. rewrite ?EFinB leeB// lee_subl_addr// -[v n]fineK// -EFinD lee_fin. by rewrite ler_distlDr// ltW//; near: n; apply: cvgr_dist_lt. have NyE u v x : u @ F --> -oo -> v @ F --> x%:E -> u \+ v @ F --> -oo. move=> /cvgeNyPle/= foo /fine_cvgP -[Fg gb]; apply/cvgeNyPleNy. near=> A; near=> n; have /(_ _)/wrap[//|Fgn] := near Fg n. rewrite -lee_subr_addr// (@le_trans _ _ (A - (x + 1))%:E)//; first by near: n. rewrite ?EFinB ?EFinD leeB// -[v n]fineK// -EFinD lee_fin. by rewrite ler_distlCDr// ltW//; near: n; apply: cvgr_dist_lt. have yyE u v : u @ F --> +oo -> v @ F --> +oo -> u \+ v @ F --> +oo. move=> /cvgeyPge foo /cvgeyPge goo; apply/cvgeyPge => A; near=> y. by rewrite -[leLHS]adde0 leeD//; near: y; [apply: foo|apply: goo]. have NyNyE u v : u @ F --> -oo -> v @ F --> -oo -> u \+ v @ F --> -oo. move=> /cvgeNyPle foo /cvgeNyPle goo; apply/cvgeNyPle => A; near=> y. by rewrite -[leRHS]adde0 leeD//; near: y; [apply: foo|apply: goo]. have addfC u v : u \+ v = v \+ u. by apply/funeqP => x; rewrite /= addeC. move: a b => [a| |] [b| |] //= _; rewrite ?(addey, addye, addeNy, addNye)//=; do ?by [apply: yE|apply: NyE|apply: yyE|apply: NyNyE]. - move=> /fine_cvgP[Ff fa] /fine_cvgP[Fg ga]; rewrite -EFinD. apply/fine_cvgP; split. by near do [rewrite fin_numD; apply/andP; split]. apply: (@cvg_trans _ ((fine \o f) \+ (fine \o g) @ F))%R; last exact: cvgD. by apply: near_eq_cvg; near do rewrite /= fineD//. - by move=> /[swap]; rewrite addfC; apply: yE. - by move=> /[swap]; rewrite addfC; apply: NyE. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule