proposition: Lemma lime_supD f g a : lime_sup f a +? lime_sup g a -> lime_sup (f \+ g)%E a <= lime_sup f a + lime_sup g a.
proof: Proof. move=> fg; rewrite !lime_sup_lim -limeD//; last first. by rewrite -!lime_sup_lim. apply: lee_lim => //. - apply: nondecreasing_at_right_is_cvge; near=> e => x y; rewrite !in_itv/=. by move=> /andP[? ?] /andP[? ?] xy; apply: leeD => //; exact: sup_ball_le. - near=> a0; apply: ub_ereal_sup => _ /= [a1 [a1ae a1a]] <-. by apply: leeD; apply: ereal_sup_ub => /=; exists a1. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)