`sigmaT_finite` lemma not available with earlier versions

[affeldt-aist]

analysis/theories/lebesgue_measure.v

Lines 390 to 393 in 018cc5f

	(* TODO: this ought to be turned into a Let but older version of mathcomp/coq
	does not seem to allow, try to change asap *)
	Local Lemma sigmaT_finite_lebesgue_measure : sigma_finite setT lebesgue_measure.
	Proof. exact/measure_extension_sigma_finite/hlength_sigma_finite. Qed.

Ideally, Local Lemma should be a Let and we should use the generic sigmaT_finite property instead
but that causes builds to fail with earlier versions, hence the kludge.