[apply lt_O_nth_prime_n
|apply (lt_O_n_elim ? H).
intro.
- apply (witness ? ? (r*(nth_prime p \sup m))).
+ apply (witness ? ? ((r*(nth_prime p) \sup m))).
rewrite < assoc_times.
rewrite < sym_times in \vdash (? ? ? (? % ?)).
rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).