split.split.
apply smallest_factor_fact.
apply le_smallest_factor_n.
(* Andrea: ancora hint non lo trova *)
apply prime_smallest_factor_n.
split.split.
apply smallest_factor_fact.
apply le_smallest_factor_n.
(* Andrea: ancora hint non lo trova *)
apply prime_smallest_factor_n.