Using the main theorem directly

This example imports only MainTheorem.lean. A caller supplies a StationaryW12LocMap package and immediately obtains both the monotonicity formula and the monotonicity inequality for the weak energy density associated with the package's displayed weak gradient.