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.
(* 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':
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.
(******************************************************************************)
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.
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.
(*