Fixing proofs on CI

[karthikbhargavan]

This PR improves the performance of some ML-KEM and ML-DSA proofs to help them pass on the CI machine.
There is still some work to be done here.

To measure the worst-performing functions, I use the following command on the logs generated:

cat log | sed -n 's/^[^(]*(\([^)]*)\)).*in \([0-9]*\) milliseconds .*/\2 \1/p' | sort -r -n -k1

I then addressed the top few failing queries by rewriting their proofs.

[W95Psp]

Looks good to me, just a few nits!

[franziskuskiefer]

lgtm with a few nits.

Also, the said we wanted to reduce large F* blobs by moving things out. We should do that whenever we touch something. It's fine to get it in like this, but let's start improving things when touching them.

[franziskuskiefer]

The C code needs updating