The following lemmas cannot be proved with Colibri using Why3.
real.mlw
However, with the SMT2 files generated for CVC5, Colibri proves unsat on all goals: