From: Cristian Armentano <??>
Date: Mon, 17 Sep 2007 22:42:30 +0000 (+0000)
Subject: temporary changes, before the complete cancellation of the file.
X-Git-Tag: make_still_working~6007
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e5025e47c9354d1bccdcbc5408579d305a493620;p=helm.git

temporary changes, before the complete cancellation of the file.
---

diff --git a/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma b/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma
index 7a68a5bd8..f26f0ea00 100644
--- a/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma
+++ b/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma
@@ -24,7 +24,7 @@ include "nat/iteration2.ma".
  *)
 
 (* some basic properties of and - or*)
-theorem andb_sym: \forall A,B:bool.
+(*theorem andb_sym: \forall A,B:bool.
 (A \land B) = (B \land A).
 intros.
 elim A;
@@ -60,7 +60,7 @@ rewrite > H1.
 rewrite > H2.
 reflexivity.
 qed.
-
+*)
 (*properties about relational operators*)
 
 theorem Sa_le_b_to_O_lt_b: \forall a,b:nat.
@@ -70,6 +70,7 @@ elim H;
   apply lt_O_S.
 qed.
 
+
 theorem n_gt_Uno_to_O_lt_pred_n: \forall n:nat.
 (S O) \lt n \to O \lt (pred n).
 intros.