Don't redefine [plus]

I dug a bit more after Andrej's comment, and discovered that (unlike in
vanilla Coq), we have to explicitly import Coq.Init.Peano to get [plus].
But it's there, so we should use it.