A compiling version of the library.

[helm.git] / matita / library / nat / times.ma

diff --git a/matita/library/nat/times.ma b/matita/library/nat/times.ma
index 2ae5ffd749b745783a2cf8c3eded7166cc4f8108..c2f25e73146383c3e6abba98595eea14b1245161 100644 (file)
--- a/matita/library/nat/times.ma
+++ b/matita/library/nat/times.ma
@@ -51,6 +51,13 @@ rewrite < plus_n_O.
 reflexivity.
 qed.
 
+theorem times_SSO_n : \forall n:nat. n + n = S (S O) * n.
+intros.
+simplify.
+rewrite < plus_n_O.
+reflexivity.
+qed.
+
 theorem symmetric_times : symmetric nat times. 
 unfold symmetric.
 intros.elim x.