(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/".
+
include "nat/div_and_mod.ma".
include "nat/factorial.ma".
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.