X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ftimes.ma;h=57dc60c6f2a071b5e25400161da998fa88f12763;hb=c99a38b6539be1eb667cced1eed2db3fc75e3162;hp=2ae5ffd749b745783a2cf8c3eded7166cc4f8108;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/matita/library/nat/times.ma b/helm/software/matita/library/nat/times.ma
index 2ae5ffd74..57dc60c6f 100644
--- a/helm/software/matita/library/nat/times.ma
+++ b/helm/software/matita/library/nat/times.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/times".
-
 include "nat/plus.ma".
 
 let rec times n m \def 
@@ -21,7 +19,6 @@ let rec times n m \def
  [ O \Rightarrow O
  | (S p) \Rightarrow m+(times p m) ].
 
-(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y).
 
 theorem times_n_O: \forall n:nat. O = n*O.
@@ -43,6 +40,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 +58,34 @@ 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.
+
+alias num (instance 0) = "natural number".
+lemma times_SSO: \forall n.2*(S n) = S(S(2*n)).
+intro.simplify.rewrite < plus_n_Sm.reflexivity.
+qed.
+
+theorem or_eq_eq_S: \forall n.\exists m. 
+n = (S(S O))*m \lor n = S ((S(S O))*m).
+intro.elim n
+  [apply (ex_intro ? ? O).
+   left.reflexivity
+  |elim H.elim H1
+    [apply (ex_intro ? ? a).
+     right.apply eq_f.assumption
+    |apply (ex_intro ? ? (S a)).
+     left.rewrite > H2.
+     apply sym_eq.
+     apply times_SSO
+    ]
+  ]
+qed.
+
 theorem symmetric_times : symmetric nat times. 
 unfold symmetric.
 intros.elim x.