proposition: Lemma nondecreasing_seqD T (d : unit) (R : numDomainType) (f g : (T -> R)^nat) : (forall x, nondecreasing_seq (f ^~ x)) -> (forall x, nondecreasing_seq (g ^~ x)) -> (forall x, nondecreasing_seq ((f \+ g) ^~ x)).
proof: Proof. by move=> ndf ndg t m n mn; apply: lerD; [exact/ndf|exact/ndg]. 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