X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FR%2Froot.ma;h=50f98d9a9732ebe9673bb7f2729afe61f64898cc;hb=a79bf6edc13daaea8135ca71fdc92e02e229f030;hp=574483be7af69191278538323f10e532c5f6741f;hpb=10dbebadd2931de5b93871a6b4989e07f668e166;p=helm.git

diff --git a/helm/software/matita/library/R/root.ma b/helm/software/matita/library/R/root.ma
index 574483be7..50f98d9a9 100644
--- a/helm/software/matita/library/R/root.ma
+++ b/helm/software/matita/library/R/root.ma
@@ -109,7 +109,7 @@ letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x);
    rewrite < sym_Rplus;apply Rle_minus_r_to_l;
    apply (pos_z_to_le_Rtimes_Rtimes_to_lt ? ? (n*Rexp_nat a (n-1)))
    [apply pos_times_pos_pos
-    [lapply (nat_lt_to_R_lt ?? H1);autobatch
+    [apply (nat_lt_to_R_lt ?? H1);
     |elim daemon]
    |rewrite > Rtimes_x_R0;do 2 rewrite > distr_Rtimes_Rplus_l;
     rewrite > sym_Rtimes in ⊢ (? ? (? (? ? (? ? (? %))) ?));
@@ -127,14 +127,16 @@ letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x);
      rewrite < distr_Rtimes_Rplus_l;
      apply (trans_Rle ? (Rexp_nat a n - Rexp_nat y n)) 
      [apply Rle_plus_l;left;autobatch
-     |rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%));
+     | cut (∀x,y.(S x ≤ y) = (x < y));[2: intros; reflexivity]
+       (* 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]]
     |intro;apply (irrefl_Rlt (n*Rexp_nat a (n-1)));
      rewrite > H11 in ⊢ (?%?);apply pos_times_pos_pos
-     [lapply (nat_lt_to_R_lt ?? H1);autobatch
+     [apply (nat_lt_to_R_lt ?? H1);
      |elim daemon]]]]
 |elim (R_archimedean R1 ((x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1)))) 
  [|autobatch]
@@ -155,13 +157,13 @@ letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x);
      assumption
     |apply lt_R0_Rinv;apply pos_times_pos_pos
      [apply pos_times_pos_pos
-      [lapply (nat_lt_to_R_lt ?? H1);autobatch
+      [apply (nat_lt_to_R_lt ?? H1);
       |elim daemon]
      |apply (trans_Rlt ???? H8);apply pos_times_pos_pos
       [apply Rlt_plus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0;
        assumption
       |apply lt_R0_Rinv;apply pos_times_pos_pos
-       [lapply (nat_lt_to_R_lt ?? H1);autobatch
+       [apply (nat_lt_to_R_lt ?? H1);
        |elim daemon]]]]]
   |split
    [(* show that h > R0, also useful in previous parts of the proof *)
@@ -247,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 ⊢ (?%?);
@@ -366,7 +368,8 @@ qed.
 lemma root_root_times : ∀x,n,m,H,H1,H2.root m (root n x H H1) H2 ? =
                           root (m*n) x ? H1.
 [cases (root_sound n x H H1);assumption
-|autobatch
+| change in match O with (O*O); apply lt_times; assumption; 
+  (* autobatch paramodulation; non fa narrowing, non fa deep subsumption... *) 
 |intros;lapply (Rexp_nat_Rexp_nat_Rtimes (root m (root n x H H1) H2 ?) m n)
  [cases (root_sound n x H H1);assumption
  |cases (root_sound m (root n x H H1))