Default Behavior for Lemma File and Module Import in Kontrol

I propose a default setting enhancement for lemma files and module imports for the kontrol build command.
Current Requirement:

If a user wants to include project-specific lemmas, he must explicitly specify the lemmas file and module import on each build, like so:

kontrol build --require lemmas.k --module-import CronTwoTest:CRON-TWO-LEMMAS

Proposed Default Behavior:

The new behavior turns this configuration into a convention:

1. We let --require default to project-lemmas.k.
2. We let--module-import default to PROJECT-LEMMAS.
3. We auto-create project-lemmas.k with an empty PROJECT-LEMMAS module if not present. (Maybe we could even add a simple lemma here, so users have a template to start from).
4. We emit a warning/error if PROJECT-LEMMAS module is missing (e.g. because a user deleted it).

This simplifies the process, benefiting users by reducing repetitive command-line specifications.

Start at the kontrol build command and inspect how --require and --module-import are currently handled. Use the proposed project-lemmas.k file and PROJECT-LEMMAS module behavior as the acceptance criteria: defaults should work without repeated flags, the file should be created when absent, and missing modules should produce a warning or error.