integrals w.r.t. lebesgue_measure and completed_lebesgue_measure agree

```coq
Lemma lebesgue_borel_int_eq (f : R -> \bar R) :
  measurable_fun (T := g_sigma_algebraType (R.-ocitv.-measurable)) setT f ->
  \int[lebesgue_measure]_x f x = \int[completed_lebesgue_measure]_x f x.
```

Is there a way to do this proof? `eq_measure_integral` does not seem to work because the measure_display is not the same.