-apply le_to_or_lt_eq.apply le_O_n.
-(* O < r *)
-cut O < r \lor O = r.
-elim Hcut1.assumption.
-apply False_ind.
-apply not_eq_O_S (S m1).
-rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
-apply le_to_or_lt_eq.apply le_O_n.
-(* prova del cut *)
-apply plog_aux_to_exp (S(S m1)).
-apply lt_O_nth_prime_n.
-assumption.
-(* fine prova cut *)
-assumption.
-(* e adesso l'ultimo goal *)
+apply le_to_or_lt_eq.apply le_O_n.assumption.
+(* e adesso l'ultimo goal. TASSI: che ora non e' piu' l'ultimo :P *)