* Obsolete debugging comments removed

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

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index b7ef49121cb2f77e39917294677a1dc9bcf192ec..be1d79b1d265c3fb50f059015b8a5fda4058f1f1 100644 (file)
--- 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.