proposition: Lemma limn_infD u v : cvgn u -> cvgn v -> limn_inf (u \+ v) = limn_inf u + limn_inf v.
proof: Proof. move=> cu cv; rewrite (cvg_limn_infE cu) -(cvg_limn_supE cu). rewrite (cvg_limn_infE cv) -(cvg_limn_supE cv) -limn_supD//. rewrite cvg_limn_supE; last exact: (@is_cvgD _ _ _ _ _ _ _ cu cv). by rewrite cvg_limn_infE //; exact: (@is_cvgD _ _ _ _ _ _ _ cu cv). Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau