About JM equality

Prove directly ( i.e. without using Leibniz equality eq) the following statement.

Lemma plus_assoc_JM : forall n p q:nat,
                       JMeq (n+(p+q)) (n+p+q).

Solution

Look at this file .