A few extensions for the moebius inversion theorem

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

diff --git a/matita/library/nat/times.ma b/matita/library/nat/times.ma
index c2f25e73146383c3e6abba98595eea14b1245161..24a2846d7a684eb337f932d502fcc6fb9dab206f 100644 (file)
--- 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.