cut S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n)).
rewrite > Hcut.assumption.
apply plus_to_minus.
cut S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n)).
rewrite > Hcut.assumption.
apply plus_to_minus.