-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)).
+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))).