X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ftimes.ma;h=24a2846d7a684eb337f932d502fcc6fb9dab206f;hb=d00c40ed72c98a6d6941e81ea16e234903996b07;hp=c2f25e73146383c3e6abba98595eea14b1245161;hpb=68a2f8d0a8c34cb7ea0438c7db9222a853a38826;p=helm.git

diff --git a/helm/software/matita/library/nat/times.ma b/helm/software/matita/library/nat/times.ma
index c2f25e731..24a2846d7 100644
--- a/helm/software/matita/library/nat/times.ma
+++ b/helm/software/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.