temporary changes, before the complete cancellation of the file.

[helm.git] / helm / software / matita / library / nat / propr_div_mod_lt_le_totient1_aux.ma

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 9751143068b5790e894772c2264c2d5c688d5702..f26f0ea004f5ce5f5c8d8df6d9c3c56d40ef5fae 100644 (file)
--- 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.
@@ -102,8 +103,7 @@ apply (le_times_to_le c (a/c) a)
 [ assumption
 | rewrite > (sym_times c (a/c)).
   rewrite > (NdivM_times_M_to_N a c) in \vdash (? % ?)
-  [ rewrite < (sym_times a c).
-    apply (O_lt_const_to_le_times_const).
+  [ apply (le_times_n c a ?).   
     assumption
   | assumption
   | assumption
@@ -152,18 +152,6 @@ cut(O \lt c)
 ]
 qed.
 
-(*
-theorem div_times_to_eqSO: \forall a,d:nat.
-O \lt d \to a*d = d \to a = (S O).
-intros.
-apply (inj_times_r1 d)
-[ assumption
-| rewrite > sym_times.
-  rewrite < (times_n_SO d).
-  assumption
-]
-qed.*)
-
 
 theorem div_mod_minus:
 \forall a,b:nat. O \lt b \to
@@ -175,22 +163,6 @@ rewrite > (div_mod a b) in \vdash (? ? ? (? % ?))
 ]
 qed.
 
-(*
-theorem sum_div_eq_div: \forall a,b,c:nat.
-O \lt c \to b \lt c \to c \divides a \to (a+b) /c = a/c.
-intros.
-elim H2.
-rewrite > H3.
-rewrite > (sym_times c n2).
-rewrite > (div_plus_times c n2 b)
-[ rewrite > (div_times_ltO n2 c)
-  [ reflexivity
-  | assumption
-  ]
-| assumption
-]
-qed.
-*)
 
 (* A corollary to the division theorem (between natural numbers).
  *