Formalization of the Lebesgue measure in Mizar

Hi all.

I'm a former math grad student, and I'm starting to learn Mizar.
My goal is to understand the challenges in computerized proof assistants
better.
(I looked at some proof assistants, and it seems Mizar has relatively good
features for mathematical abstraction, with Ghilbert maybe a little better
but with a tiny library)

So I picked an area of the mathematical space I'm familiar with but with
little coverage in Mizar - the Lebesgue measure - and not I'm trying to
prove some well-known theorems about it.
I'm having some trouble with writing proofs in Mizar and would be glad if
you could help me out.

My working directory is publicly available at
https://github.com/amirlb/mizar-lebesgue-measure

1. Is this really not covered? AFAICT, the Lebesgue measure only appears in
two definitions in the end of MEASURE7. If it is covered, or if anyone else
is in the process of formalizing this, I'll pick another area.

2. Is my coding style good? Are there any theorems that would be better
represented as clusters? Or some other changes? Also, my proofs seems very
long while containing little actual mathematics, is there some kind of
optimization I'm missing?
(But the proof of e.g. MEASURE7:Th1 is long as well, so I don't have much
hope for any proof involving sequences)

3. Some of the inference chains make the Mizar engine seem "less smart"
than others. For instance, the end of the proof of EmptySetMeasureZero. Or
algebraic manipulations, such as
        A5: c > a;
        set b = (a + c) / 2;
        a + c > a + a by A5, XREAL_1:6;
        then (a + c) / 2 > (a + a) / 2 by XREAL_1:74;
        then A6: b > a;
which would be nicer if it had equalities instead of inequalities.

4. I found almost no documentation of the system, especially its semantics.
My resources are Freek Wiedijk's tutorial, the Mizar Manual, skimming the
PC Mizar book, and a few pages on the TWiki (list of articles, list of
error messages). So in many cases, when I have a problem I'm trying all
kinds of stuff randomly until one thing works. For example, I don't
understand the difference between Real and Element of REAL. As another
example, I don't know what the "correctness" stanza of a registration
should justify. Are there any more sources to learn about Mizar?

5. I can't find documentation for the smarter tools - MML query, Proof
advisor, MoMM. So I don't use them, and this is probably slowing me down.
Can you point me to their documentation?


I will appreciate any sort of ideas, response or discussion.


Thanks in advance,
Amir