Comment by joseraul

All this may become much easier when we manage to merge proof assistants with automatic provers.

Here is how you can prove the first theorem in Dafny. https://rise4fun.com/Dafny/GxplK