cut ((S(S m1)) = r).
rewrite > Hcut3 in \vdash (? (? ? %)).
change with (nth_prime p \divides r \to False).
intro.
apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
apply lt_SO_nth_prime_n.
cut ((S(S m1)) = r).
rewrite > Hcut3 in \vdash (? (? ? %)).
change with (nth_prime p \divides r \to False).
intro.
apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
apply lt_SO_nth_prime_n.