[kachnuv_ocasek]

Lean has much better UX to be frank. Rocq is fine, but if I were to start formalising today, I'd pick Lean.