Fill finite additivity of counting measure

[Chessing234]

Fill finite additivity of counting measure using Set.encard_union_eq, followed by the additive coercion into EReal. The previous proof referenced the nonexistent ENat.card_union_eq_add_card_of_disjoint.

Validation: an isolated Lean check with the actual structure and counting-measure declaration fails for the old proof and passes for the corrected declaration.

Full chapter validation is blocked by existing errors in Sections 1.4.1–1.4.3. PR #711 repairs Sections 1.4.1 and 1.4.2, but Section 1.4.3 still fails. The default root currently omits Section 1.4.3, so the ordinary CI check does not validate this change. Keeping this draft until the shared chapter builds.

[teorth]

Thanks — the content here is good, and I've merged 29 of the sibling PRs from this batch (#686–#718). This one now needs a rebase onto main before it can go in.

The conflict is purely positional, not substantive: a sibling PR filled other fields of the same structure literal, and git can't line up the context. Concretely, one side of the conflict has the fields that sibling filled (with your field still sorry), and the other side has your field filled (with theirs still sorry). The resolution is just the union — take whichever side has the real proof for each field, discarding the sorry version.

I resolved all four of the conflicting PRs that way locally and ran a full lake build: 8310 jobs, no errors. So this is mechanical, and nothing about your proof needs to change.

One suggestion for future batches, since this cost four PRs a round-trip: when several PRs fill different fields of the same structure literal, they will always conflict with each other even though each is individually mergeable against main. Grouping the fields of one structure into a single PR avoids it entirely — and would be easier to review, too.

[Chessing234]

rebased onto main. kept each field that already had a proof, and the one this pr fills.