proposition: Lemma lim_cst {U} {F} {FF : ProperFilter F} (k : T) : lim ((fun _ : U => k) @ F) = k.
proof: Proof. by apply: cvg_lim; apply: cvg_cst. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed