proposition: Lemma lim_mkord (R : realFieldType) (P : {pred nat}) (f : (\bar R)^nat) : limn (fun n => \sum_(k < n | P k) f k)%E = \sum_(k <oo | P k) f k.
proof: Proof. rewrite (_ : (fun n => _) = (fun n => \sum_(0 <= k < n | P k) f k)%E) //. by rewrite funeqE => k; rewrite big_mkord. 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