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

diff --git a/matita/library/nat/times.ma b/matita/library/nat/times.ma
index 2ae5ffd74..24a2846d7 100644
--- a/matita/library/nat/times.ma
+++ b/matita/library/nat/times.ma
@@ -43,6 +43,16 @@ reflexivity.
 apply assoc_plus.
 qed.
 
+theorem times_O_to_O: \forall n,m:nat.n*m = O \to n = O \lor m= O.
+apply nat_elim2;intros
+  [left.reflexivity
+  |right.reflexivity
+  |apply False_ind.
+   simplify in H1.
+   apply (not_eq_O_S ? (sym_eq  ? ? ? H1))
+  ]
+qed.
+
 theorem times_n_SO : \forall n:nat. n = n * S O.
 intros.
 rewrite < times_n_Sm.
@@ -51,6 +61,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.