proposition: Lemma le_nseries (u : nat^nat) : {homo nseries u : a b / a <= b}%N.
proof: Proof. move=> a b ab; rewrite /nseries [in X in (_ <= X)%N]/index_iota subn0. rewrite -[in X in (_ <= X)%N](subnKC ab) iotaD big_cat/= add0n. by rewrite /index_iota subn0 leq_addr. 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