X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=3db29f622fb95a5e096cb46744928c97bcef9f39;hb=8ef11a4b981e6da3d60f353386b17f7692dc0ecd;hp=9bbce8144ff8885a7c7346bdb9b7937983bd5f7e;hpb=6db38e3d8e4083765f2fce40c7845c9827b9afd0;p=helm.git

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index 9bbce8144..3db29f622 100644
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/gcd".
-
 include "nat/primes.ma".
 include "nat/lt_arith.ma".
 
@@ -101,7 +99,6 @@ qed.
 theorem divides_gcd_nm: \forall n,m.
 gcd n m \divides m \land gcd n m \divides n.
 intros.
-(*CSC: simplify simplifies too much because of a redex in gcd *)
 change with
 (match leb n m with
   [ true \Rightarrow 
@@ -594,7 +591,6 @@ intro.apply (nat_case n)
 qed.
 
 theorem symmetric_gcd: symmetric nat gcd.
-(*CSC: bug here: unfold symmetric does not work *)
 change with 
 (\forall n,m:nat. gcd n m = gcd m n).
 intros.
@@ -904,3 +900,35 @@ cut (n \divides p \lor n \ndivides p)
  ]
 qed.
 
+(*
+theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H5 in H4.
+elim (divides_times_to_divides ? ? ? H1 H4)
+  [elim H.apply False_ind.
+   apply H2.apply sym_eq.apply H8
+    [assumption
+    |apply prime_to_lt_SO.assumption
+    ]
+  |elim H6.
+   apply (witness ? ? n1).
+   rewrite > assoc_times.
+   rewrite < H7.assumption
+  ]
+qed.
+*)
+
+theorem divides_to_divides_times: \forall p,q,n. prime p  \to p \ndivides q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H4 in H2.
+elim (divides_times_to_divides ? ? ? H H2)
+  [apply False_ind.apply H1.assumption
+  |elim H5.
+   apply (witness ? ? n1).
+   rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+   rewrite > assoc_times.
+   rewrite < H6.assumption
+  ]
+qed.
\ No newline at end of file