The Coq mailing list

[leonardomatiasrodriguez AT gmail.com]

Hi! This is my first post.
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.
But i'm stuck after the intros tactic (jaja!)
Any hint will be appreciated
Thanks you in advance
Leo