Someody42

You can absolutely do constructive things in Lean, as long as you use neither the built-in "quot" type nor the three other axioms described in the docs, and then you get a system with all the desired properties I think

In theory yes, but there are two main things that makes it harder :

- some technical details have changed. They don't affect the axiomatic aspects of Lean, but they force us to redefine some things in a cleaner way.

- we don't only want to port the theorem. We want to port them to a human-readable proof that can be easily maintained