Minor changes pro-automation

[helm.git] / helm / software / matita / library / R / root.ma

diff --git a/helm/software/matita/library/R/root.ma b/helm/software/matita/library/R/root.ma
index 1205fc92b94071bc3bd168d7e70fd8f0e463b37d..50f98d9a9732ebe9673bb7f2729afe61f64898cc 100644 (file)
--- a/helm/software/matita/library/R/root.ma
+++ b/helm/software/matita/library/R/root.ma
@@ -128,17 +128,12 @@ letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x);
      apply (trans_Rle ? (Rexp_nat a n - Rexp_nat y n)) 
      [apply Rle_plus_l;left;autobatch
      | cut (∀x,y.(S x ≤ y) = (x < y));[2: intros; reflexivity]
-       applyS Rexp_nat_tech;
-       [ unfold lt; change in H1 with (O < n);
-         autobatch; (*applyS H1;*)
-       | assumption;
-       | elim daemon; ]]
-      (*  
+       (* applyS Rexp_nat_tech by sym_Rtimes, assoc_Rtimes;*)
       rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%));
       rewrite < assoc_Rtimes;apply Rexp_nat_tech
       [autobatch
       |assumption
-      |(* by transitivity y^n < x < a^n and injectivity *) elim daemon]]*)
+      |(* by transitivity y^n < x < a^n and injectivity *) elim daemon]]
     |intro;apply (irrefl_Rlt (n*Rexp_nat a (n-1)));
      rewrite > H11 in ⊢ (?%?);apply pos_times_pos_pos
      [apply (nat_lt_to_R_lt ?? H1);
@@ -254,7 +249,7 @@ intro;elim f;simplify
  |simplify;cases z;simplify
   [1,3:autobatch
   |rewrite < plus_n_O;rewrite > plus_n_O in ⊢ (?%?);
-   apply lt_plus;autobatch]
+   apply lt_plus;autobatch depth=2]
  |simplify;cases z;simplify;
   [1,3:autobatch
   |rewrite < plus_n_O;rewrite > (times_n_O O) in ⊢ (?%?);