rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
rewrite > H6.reflexivity.
rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
rewrite > H6.reflexivity.