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