-change in match p + n * (S p) with (pred ((S n) * (S p))).
-change in match q + n * (S q) with (pred ((S n) * (S q))).
+change in match (p + n * (S p)) with (pred ((S n) * (S p))).
+change in match (q + n * (S q)) with (pred ((S n) * (S q))).
rewrite < nat_compare_pred_pred.
rewrite < nat_compare_times_l.
rewrite < nat_compare_S_S.
rewrite < nat_compare_pred_pred.
rewrite < nat_compare_times_l.
rewrite < nat_compare_S_S.