proposition: Lemma incr_S1 N : nondecreasing_seq (S1 N).
proof: Proof. apply/nondecreasing_seqP => n; rewrite /S1. have [nN|Nn] := leqP n N; first by rewrite !big_geq // (leq_trans nN). by rewrite big_nat_recr//= lerDl exp_coeff_ge0 // ltW. 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