Require Coq.Arith.Plus.
Read Module Coq.Arith.Minus.
Locate Library Coq.Arith.Minus.