X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Ftimes.ma;h=c2f25e73146383c3e6abba98595eea14b1245161;hb=7f82161596bdfccc1179f5edcc0bfd76d34516b5;hp=2ae5ffd749b745783a2cf8c3eded7166cc4f8108;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/library/nat/times.ma b/matita/library/nat/times.ma
index 2ae5ffd74..c2f25e731 100644
--- 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.