split.split.
apply smallest_factor_fact.
apply le_smallest_factor_n.
-(* ancora hint non lo trova *)
+(* Andrea: ancora hint non lo trova *)
apply prime_smallest_factor_n.
change with (S(S O)) \le S (fact (S n1)).
apply le_S.apply le_SSO_fact.
change with prime (S(S O)).
apply primeb_to_Prop (S(S O)).
intro.
-(* ammirare la resa del letin !! *)
change with
let previous_prime \def (nth_prime m) in
let upper_bound \def S (fact previous_prime) in