X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=be1d79b1d265c3fb50f059015b8a5fda4058f1f1;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=b7ef49121cb2f77e39917294677a1dc9bcf192ec;hpb=7efb15b93cf42eae8b34a12a327ee7213c1dbecc;p=helm.git

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index b7ef49121..be1d79b1d 100644
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -482,17 +482,6 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 qed.
 
-(* esempio di sfarfallalmento !!! *)
-(*
-theorem bad: \forall n,p,q:nat.prime n \to divides n (p*q) \to
-divides n p \lor divides n q.
-intros.
-cut divides n p \lor \not (divides n p).
-elim Hcut.left.assumption.
-right.
-cut \exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O).
-elim Hcut1.elim H3.*)
-
 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to
 divides n p \lor divides n q.
 intros.