(S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb.
intros.
cut upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime).
rewrite < Hcut in \vdash (? % ?).
apply le_min_aux.
apply plus_to_minus.
(S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb.
intros.
cut upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime).
rewrite < Hcut in \vdash (? % ?).
apply le_min_aux.
apply plus_to_minus.