* Obsolete debugging comments removed

* Debugging comments by Andrea marked with "Andrea:"

diff --git a/helm/matita/library/higher_order_defs/functions.ma b/helm/matita/library/higher_order_defs/functions.ma
index d2a577a4912145a0621ced90440568fb039c4359..321ae46b7502c1578975b24ccdc25c4351065788 100644 (file)
--- a/helm/matita/library/higher_order_defs/functions.ma
+++ b/helm/matita/library/higher_order_defs/functions.ma
@@ -20,7 +20,6 @@ definition injective: \forall A,B:Type.\forall f:A \to B.Prop
 \def \lambda A,B.\lambda f.
   \forall x,y:A.f x = f y \to x=y.
 
-(* we have still to attach exists *)
 definition surjective: \forall A,B:Type.\forall f:A \to B.Prop
 \def \lambda A,B.\lambda f.
   \forall z:B. \exists x:A.z=f x.

diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index ad74a324db86b807cce2bbccc166c8a719fa83d2..73344c7c46b0cf1466b0aea949755ced792fc13a 100644 (file)
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -133,7 +133,6 @@ rewrite < sym_plus.
 apply le_plus_n.
 rewrite < sym_times.
 rewrite > distr_times_minus.
-(* ATTENZIONE ALL' ORDINAMENTO DEI GOALS *)
 rewrite > plus_minus.
 rewrite > sym_times.
 rewrite < H5.

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.

diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index 3babb5c75151fe36f0cf098e055d39294164eb22..51d0108d97d89d937a488c68d6fbb7bc1e0a5323 100644 (file)
--- a/helm/matita/library/nat/log.ma
+++ b/helm/matita/library/nat/log.ma
@@ -175,7 +175,7 @@ apply lt_div_n_m_n.assumption.assumption.assumption.
 intros.
 change with (\lnot (mod n1 m = O)).
 rewrite > H4.
-(* META NOT FOUND !!!  
+(* Andrea: META NOT FOUND !!!  
 rewrite > sym_eq. *)
 simplify.intro.
 apply not_eq_O_S m1.

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index dd4fdcbf98a1e6e5c0667907c4c080c52b0c5696..f8df1c6be9f171b1987ba7a493f344ce9e0c4521 100644 (file)
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -116,7 +116,6 @@ qed.
 theorem lt_times_to_lt_l: 
 \forall n,p,q:nat. lt (times p (S n)) (times q (S n)) \to lt p q.
 intros.
-(* convertibility problem here *)
 cut Or (lt p q) (Not (lt p q)).
 elim Hcut.
 assumption.

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 079e902ad39ba9213b28b7b58062ed9e9db39dcb..7240b7d09ebbc9f18384e68ae1d51f3dffa8021b 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -118,8 +118,8 @@ intros 2.
 apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
 intros.simplify.reflexivity.
 intros.apply False_ind.
-(* ancora problemi con il not *)
-apply not_le_Sn_O n1 H.
+apply not_le_Sn_O.
+goal 13.apply H.
 intros.
 simplify.apply H.apply le_S_S_to_le. apply H1.
 qed.

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 8035d49ddba64dcb5d207ab2e4c9179d477d4d2c..200ccba5a9086b0ca2a940c7f19ae0964bb8402c 100644 (file)
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -62,7 +62,7 @@ apply ex_intro nat ? (smallest_factor (S (fact (S n1)))).
 split.split.
 apply smallest_factor_fact.
 apply le_smallest_factor_n.
-(* ancora hint non lo trova *)
+(* Andrea: ancora hint non lo trova *)
 apply prime_smallest_factor_n.
 change with (S(S O)) \le S (fact (S n1)).
 apply le_S.apply le_SSO_fact.
@@ -98,7 +98,6 @@ apply nat_case n.
 change with prime (S(S O)).
 apply primeb_to_Prop (S(S O)).
 intro.
-(* ammirare la resa del letin !! *)
 change with
 let previous_prime \def (nth_prime m) in
 let upper_bound \def S (fact previous_prime) in

diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma
index 1c145dd6141cea519fd99f7c681a179159a72346..79640b1362f86e9a654cc55a568d766daa8e0120 100644 (file)
--- a/helm/matita/library/nat/plus.ma
+++ b/helm/matita/library/nat/plus.ma
@@ -36,11 +36,6 @@ simplify.reflexivity.
 simplify.apply eq_f.assumption.
 qed.
 
-(* some problem here: confusion between relations/symmetric 
-and functions/symmetric; functions symmetric is not in 
-functions.moo why?
-theorem symmetric_plus: symmetric nat plus. *)
-
 theorem sym_plus: \forall n,m:nat. n+m = m+n.
 intros.elim n.
 simplify.apply plus_n_O.
@@ -67,8 +62,7 @@ theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
 
 theorem injective_plus_l: \forall m:nat.injective nat nat (\lambda n.n+m).
 intro.simplify.intros.
-(* qui vorrei applicare injective_plus_r *)
-apply inj_plus_r m.
+apply injective_plus_r m.
 rewrite < sym_plus.
 rewrite < sym_plus y.
 assumption.

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index 644cae978f58a419e9d2d53ca2188b7fbcbe1322..dc5f627e43103119199d71747a837c60b8595cf4 100644 (file)
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -59,7 +59,7 @@ apply witness n m (div m n).
 rewrite > plus_n_O (n*div m n).
 rewrite < H1.
 rewrite < sym_times.
-(* perche' hint non lo trova ?*)
+(* Andrea: perche' hint non lo trova ?*)
 apply div_mod.
 assumption.
 qed.