-letin previous_prime \def nth_prime n.
-letin upper_bound \def S (fact previous_prime).
-apply lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m.
-cut S (fact (nth_prime n))-(S (fact (nth_prime n)) - (S (nth_prime n))) = (S (nth_prime n)).
+letin previous_prime \def (nth_prime n).
+letin upper_bound \def (S previous_prime!).
+apply (lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m).
+cut (S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n))).