Make mixed automatic/manual verification more ergonomic

Instead of putting proof annotations on the specifications in the Rust code, it would be better to just edit the proof files to account for manual adjustments. We need the following adjustments to the frontend:

• the part of the proof stating which other functions the code uses should be put in the spec file, to make it robust against adjustments of the code.
• the header part of the proof should be similarly part of another file. Maybe as some Ltac code?
• the proof file should just contain parts of the proof that call into Lithium + manual parts of the proof. Regeneration of the files should not override this proof file.