3 ms·

100% agree. I did not understand induction until I learned Coq. It really shows how mechanical proving can be.