How would you prove it on paper? I'd say probably not by induction. Maybe you already have the inverse of +n?

Note that there is also the lia tactic for solving linear integer arithmetic problems. You just need to import it with the following command.

From Coq Require Import Lia.