Remove admits, improve proof performance for ML-KEM

[karthikbhargavan]

We still have some admits in the proofs. Some of these are because of F* performance. (The code verifies on some machines and not others). Other admits are simply things we still need to look at and remove. We should remove them one by one, with an eye towards ML-DSA proofs.

[karthikbhargavan]

This still ongoing, likely will be folded into work on ML-DSA