Remove admits, improve proof performance for ML-KEM

[karthikbhargavan]

trafficstars

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.