The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

leonardomatiasrodriguez AT gmail.com
 wrote:
> I'm just learning Coq, and i'm proving a simple theorem:
> Theorem le_minus_minus : forall n m , n<= m ->  m - (m - n) = n.
> My idea is to replace the first occurrence of "m" in "m - (m - n)"  by "n + (m
> - n)" using
> le_plus_minus
>       : forall n m : nat, n<= m ->  m = n + (m - n)
> and then prove another lemma
>        forall n p : nat,  (n+p) - p = n.
> to conclude ( n + (m - n) ) - (m - n) = n.
>    

I see you got an answer to your question, but I'd like to point out 
another tactic that may make your life easier in the future.  The 
[rewrite] syntax, suggested by Evgeny and used in your posted solution, 
requires you to keep track of the argument orders of various lemmas.  By 
using the [replace] tactic instead, you can avoid that need.  Here's an 
alternate script using [replace] (see the manual for documentation of 
unfamiliar tactics):

Goal forall n m , n <= m -> m - (m - n) = n.
  intros.
  pattern m at 1.
  replace m with (n + (m - n)).
  apply other_lemma.
  symmetry; apply le_plus_minus; assumption.
Qed.

P.S.: I wouldn't recommend using such an unwieldy proof script in a real 
development, since this proof script also works (after you have run 
"Require Import Omega."):
    intros; omega.