HoTT/HoTT — pull request #328 by JasonGross (2014-02-27 18:07:47+00:00)
Title: 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.