- eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.