freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / dama / dama_didactic / ex_seq.ma

diff --git a/helm/software/matita/contribs/dama/dama_didactic/ex_seq.ma b/helm/software/matita/contribs/dama/dama_didactic/ex_seq.ma
index fcefda2448b1537a81b0c86e9a90f82127f364ef..53c8bf9cf0d6905b67043fecc0eee353acda27df 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_didactic/ex_seq.ma
+++ b/helm/software/matita/contribs/dama/dama_didactic/ex_seq.ma
@@ -34,7 +34,7 @@ lemma l1: monotone_not_increasing alpha.
   assume n:nat.
   we need to prove (alpha (S n) ≤ alpha n)
   or equivalently (Rdiv (alpha n) (S (S O)) ≤ alpha n).
-  by _ done.
+  done.
 qed.
  
 lemma l2: inf_bounded alpha.
@@ -54,12 +54,12 @@ lemma l2: inf_bounded alpha.
     (* approssimiamo con questo *)
     we need to prove (R0 ≤ alpha O)
     or equivalently (R0 ≤ R1).
-    by _ done.
+    done.
   case S (m:nat).
    by induction hypothesis we know (R0 ≤ alpha m) (H).
    we need to prove (R0 ≤ alpha (S m))
    or equivalently (R0 ≤ Rdiv (alpha m) (S (S O))).
-    by _ done.
+    done.
 qed.
 
 axiom xxx':
@@ -68,15 +68,16 @@ axiom xxx':
   punto_fisso F l.
 
 theorem dimostrazione: tends_to alpha O.
- by _ let l:R such that (tends_to alpha l) (H).
+ let l:R such that (tends_to alpha l) (H).
 (* unfold alpha in H.
  change in match alpha in H with (successione F O).
  check(xxx' F cont l H).*)
- by (lim_punto_fisso F R1 cont l H)  we proved (punto_fisso F l) (H2)
+(* end auto($Revision: 8612 $) proof: TIME=0.01 SIZE=100 DEPTH=100 *)
+ using (lim_punto_fisso F R1 cont l H)  we proved (punto_fisso F l) (H2)
  that is equivalent to (l = (Rdiv l (S (S O)))).
- by _ we proved (tends_to alpha l = tends_to alpha O) (H4).
+ we proved (tends_to alpha l = tends_to alpha O) (H4).
  rewrite < H4.
- by _ done.
+ done.
 qed.
 
 (******************************************************************************)
@@ -95,15 +96,15 @@ lemma uno: ∀n. alpha2 n ≥ R1.
    alias num (instance 0) = "natural number".
    we need to prove (alpha2 0 ≥ R1)
    or equivalently ((S (S O)) ≥ R1).
-   by _ done.
+   done.
  case S (m:nat).
    by induction hypothesis we know (alpha2 m ≥ R1) (H).
    we need to prove (alpha2 (S m) ≥ R1)
    or equivalently (Rmult (alpha2 m) (alpha2 m) ≥ R1).letin xxx := (n ≤ n);
-   by _ we proved (R1 · R1 ≤ alpha2 m · alpha2 m) (H1).
-   by _ we proved (R1 · R1 = R1) (H2).
+   we proved (R1 · R1 ≤ alpha2 m · alpha2 m) (H1).
+   we proved (R1 · R1 = R1) (H2).
    rewrite < H2.
-   by _ done.
+   done.
 qed.
 
 lemma mono1: monotone_not_decreasing alpha2.
@@ -112,7 +113,7 @@ lemma mono1: monotone_not_decreasing alpha2.
  assume n:nat.
  we need to prove (alpha2 n ≤ alpha2 (S n))
  or equivalently (alpha2 n ≤ Rmult (alpha2 n) (alpha2 n)).
- by _ done.
+ done.
 qed.
 
 (*