Coq proof of forall a b c: nat, b >= c -> a + b - c = a + (b - c)

Question

Does anybody know of a proof in any of the standard libraries of Coq of the following theorem? If there is one, I couldn´t find it.

forall a b c: nat, b >= c -> a + b - c = a + (b - c)

Thanks in advance, Marcus.

Answer 1

It is unlikely that somewhat specific formulations would be in the standard library. In particular, for regular Presburger arithmetic, there is a powerful tactic that is complete, namely omega:

Require Import Omega.

Theorem t : forall a b c: nat, b >= c -> a + b - c = a + (b - c).
Proof.
  intros. omega.
Qed.

Answer 2

There is a very similar lemma in the Coq standard library (checked with version 8.5pl3), it's called

Nat.add_sub_assoc
     : forall n m p : nat, p <= m -> n + (m - p) = n + m - p

Here is how it can be used:

Require Import Coq.Arith.Arith.

Goal forall a b c: nat, b >= c -> a + b - c = a + (b - c).
  intros a b c H.
  apply (eq_sym (Nat.add_sub_assoc _ _ _ H)).
Qed.

You can use Coq's search facilities to discover it:

Require Import Coq.Arith.Arith.
Search (_ + _ - _).