Problem with reproducing the proofs

I had trouble reproducing all the proofs (most of them work)
Launching `gnatprove -Pmlkem -u src/mlkem.adb`, it tells me there are 5 "Unproved".

Those are :
```
mlkem.adb:270:25: medium: assertion might fail
270 | pragma Assert (T (R) = T (X mod Q));
| ^~~~~~~~~~~~~~~~~~
```
...
```
mlkem.adb:990:14: medium: loop invariant might not be preserved by an arbitrary iteration, cannot prove Bits_12_To_U16 (B (K * 12 .. K * 12 + 11)) < Q
990 | (Bits_12_To_U16 (B (K * 12 .. K * 12 + 11)) < Q));
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
```
...
```
mlkem.adb:1614:22: medium: assertion might fail
1614 | pragma Assert (K = 128);
| ^~~~~~~
```
...
```
mlkem.adb:1671:36: medium: loop invariant might fail in first iteration
1671 | pragma Loop_Invariant (I32 (K) = 2**I + Count - J - 1);
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
```
...
```
mlkem.adb:1685:22: medium: assertion might fail
1685 | pragma Assert (K = 0);
| ^~~~~
```

I am running Ubuntu and I followed the installation in the spark_ada/README.

There was a warning `cvc4 is deprecated`, changing to cvc5 in the file `mlkem.gpr` helped, now there is only one "Unproved", which is
```
mlkem.adb:1614:22: medium: assertion might fail
1614 | pragma Assert (K = 128);
| ^~~~~~~
```

Start with the installation steps in spark_ada/README and reproduce `gnatprove -Pmlkem -u src/mlkem.adb` on Ubuntu. Compare the proof results before and after changing cvc4 to cvc5 in mlkem.gpr, then inspect the reported assertions and loop invariants in mlkem.adb. Done means the listed proof obligations are no longer reported as unproved.

Written by the indexing model from the issue text.