Comment by jjmarr

I learned coq as a teenager because the name was funny and one defined everything in terms of the `succ` function.

Never underestimate our motivation.