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