Require Import Coq.Arith.Plus.
Require Coq.Arith.Minus.
Locate Library Coq.Arith.Minus.