-change with pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
- pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p))))).
-rewrite < times_minus1 n q p H.reflexivity.
+change with (pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
+ pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p)))))).
+rewrite < (times_minus1 n q p H).reflexivity.