-cut (S (nth_prime m)!-(S (nth_prime m)! - (S (nth_prime m))) = (S (nth_prime m))).
-rewrite > Hcut.exact (smallest_factor_fact (nth_prime m)).
-(* maybe we could factorize this proof *)
-apply plus_to_minus.
-apply plus_minus_m_m.
-apply le_S_S.
-apply le_n_fact_n.
-apply le_smallest_factor_n.
+apply smallest_factor_fact.
+apply transitive_le;
+ [2: apply le_smallest_factor_n
+ | skip
+ | apply (le_plus_n_r (S (nth_prime m)) (S (fact (nth_prime m))))
+ ].