theorem prova2 :
\forall n. S n \divides (S n)!.
intros.
+(* se non trova subito sym_times poi si perde! *)
+(* alternativamente si puo' abilitare la are_convertible nella
+ is_identity, ma poi va peggio nel resto (conv lunghe) *)
+letin www \def sym_times.
+clearbody www.
applyS (witness ? ? ? (refl_eq ? ?)).
qed.