-cut i < (S n)*(S m).
-cut j < (S n)*(S m).
-cut (i \mod (S n)) < (S n).
-cut (i/(S n)) < (S m).
-cut (j \mod (S n)) < (S n).
-cut (j/(S n)) < (S m).
-rewrite > div_mod i (S n).
-rewrite > div_mod j (S n).
-rewrite < H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3.
-rewrite < H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3 in \vdash (? ? (? % ?) ?).
-rewrite < H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5.
-rewrite < H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5 in \vdash (? ? ? (? % ?)).
+cut (i < (S n)*(S m)).
+cut (j < (S n)*(S m)).
+cut ((i \mod (S n)) < (S n)).
+cut ((i/(S n)) < (S m)).
+cut ((j \mod (S n)) < (S n)).
+cut ((j/(S n)) < (S m)).
+rewrite > (div_mod i (S n)).
+rewrite > (div_mod j (S n)).
+rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
+rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
+rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
+rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).