(* -*- holl -*- *)

needs "Cartan/misc.ml";;

let ASSERT_TAC tm =
  SUBGOAL_THEN tm STRIP_ASSUME_TAC;;

let TRANS_TAC tm =
  MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC tm THEN CONJ_TAC;;

(* ------------------------------------------------------------------------- *)
(* HIGHER_COMPLEX_DERIVATIVE_COMP_LEMMA                                      *)
(* ------------------------------------------------------------------------- *)

g `!f g z s t n i.
     open s /\ f holomorphic_on s /\ z IN s /\
     open t /\ g holomorphic_on t /\ (!w. w IN s ==> f w IN t) /\
     complex_derivative f z = Cx(&1) /\
     (!i. 1 < i /\ i <= n ==> higher_complex_derivative i f z = Cx(&0)) /\
     i <= n
     ==> higher_complex_derivative i (g o f) z =
         higher_complex_derivative i g (f z)`;;
e (REPEAT GEN_TAC);;
e (SUBGOAL_THEN
    `open s /\ f holomorphic_on s /\ z IN s /\ open t /\
       (!w. w IN s ==> f w IN t) /\
       complex_derivative f z = Cx(&1) /\
       (!i. 1 < i /\ i <= n ==> higher_complex_derivative i f z = Cx(&0))
       ==> !i g. g holomorphic_on t /\ i <= n
           ==> higher_complex_derivative i (g o f) z =
               higher_complex_derivative i g (f z)`
     (fun th -> MESON_TAC [th]));;
e STRIP_TAC;;
e (INDUCT_TAC THEN
   REWRITE_TAC [LE_SUC_LT; higher_complex_derivative_alt; o_THM]);;
e (REPEAT STRIP_TAC);;
e (TRANS_TAC `higher_complex_derivative i
              (\w. complex_derivative g (f w) * complex_derivative f w) z`);;
e (MATCH_MP_TAC HIGHER_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN);;
e (EXISTS_TAC `s:complex->bool`);;
e (ASM_REWRITE_TAC []);;
e (REPEAT CONJ_TAC);;
e (MATCH_MP_TAC HOLOMORPHIC_COMPLEX_DERIVATIVE);;

e (ASM_REWRITE_TAC []);;
e (MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE);;
e (EXISTS_TAC `t:complex->bool`);;
e (ASM_SIMP_TAC []);;
e (MATCH_MP_TAC HOLOMORPHIC_ON_MUL);;
e CONJ_TAC;;
e (REWRITE_TAC [GSYM o_DEF]);;
e (MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE);;
e (EXISTS_TAC `t:complex->bool`);;
e (ASM_REWRITE_TAC []);;
e (MATCH_MP_TAC HOLOMORPHIC_COMPLEX_DERIVATIVE);;
e (ASM_REWRITE_TAC []);;
e (ASM_REWRITE_TAC [ETA_AX]);;
e (MATCH_MP_TAC HOLOMORPHIC_COMPLEX_DERIVATIVE);;
e (ASM_REWRITE_TAC []);;
e (REPEAT STRIP_TAC);;
e (MATCH_MP_TAC COMPLEX_DERIVATIVE_CHAIN);;
e (ASM_MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;
e (TRANS_TAC
     `vsum (0..i)
        (\j. Cx (&(binom (i,j))) *
             higher_complex_derivative j (\w. complex_derivative g (f w)) z *
             higher_complex_derivative (i - j) (complex_derivative f) z)`);;
e (MATCH_MP_TAC HIGHER_COMPLEX_DERIVATIVE_MUL);;
e (EXISTS_TAC `s:complex->bool`);;
e (ASM_REWRITE_TAC []);;
e (ASM_SIMP_TAC [HOLOMORPHIC_COMPLEX_DERIVATIVE]);;
e (REWRITE_TAC [GSYM o_DEF]);;
e (MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE);;
e (EXISTS_TAC `t:complex->bool`);;
e (ASM_REWRITE_TAC []);;
e (ASM_SIMP_TAC [HOLOMORPHIC_COMPLEX_DERIVATIVE]);;
e (REWRITE_TAC [GSYM higher_complex_derivative_alt]);;
e (TRANS_TAC
     `vsum (i..i)
        (\j. Cx (&(binom (i,j))) *
             higher_complex_derivative j (\w. complex_derivative g (f w)) z *
             higher_complex_derivative (SUC (i - j)) f z)`);;
e (MATCH_MP_TAC VSUM_SUPERSET);;
e (REWRITE_TAC [SUBSET_NUMSEG; LT_REFL; LE_0; LE_REFL; IN_NUMSEG_0; NUMSEG_SING; IN_SING]);;
e (X_GEN_TAC `j:num`);;
e (REWRITE_TAC [ARITH_RULE `j <= i /\ ~(j = i) <=> j < i`]);;
e (DISCH_TAC);;
e (ASSERT_TAC `1 < SUC (i - j) /\ SUC (i - j) <= n`);;
e (ASM_SIMP_TAC [ARITH_RULE `i < n /\ j < i ==> 1 < SUC (i - j) /\ SUC (i - j) <= n`]);;
e (MATCH_MP_TAC (ARITH_RULE `i < n /\ j < i ==> 1 < SUC (i - j)`));;
e (ASM_REWRITE_TAC []);;
e (ASM_SIMP_TAC [COMPLEX_MUL_RZERO; COMPLEX_VEC_0]);;
e (REWRITE_TAC [NUMSEG_SING; VSUM_SING; BINOM_REFL; SUB_REFL]);;
e (ASM_REWRITE_TAC [COMPLEX_MUL_LID; COMPLEX_MUL_RID; higher_complex_derivative]);;
e (ASM_REWRITE_TAC [GSYM o_DEF]);;
e (REWRITE_TAC [GSYM higher_complex_derivative; higher_complex_derivative_alt]);;
e (FIRST_X_ASSUM MATCH_MP_TAC);;
e (ASM_SIMP_TAC [ARITH_RULE `i < n ==> i <= n`]);;
e (MATCH_MP_TAC HOLOMORPHIC_COMPLEX_DERIVATIVE);;
e (ASM_REWRITE_TAC []);;
let HIGHER_COMPLEX_DERIVATIVE_COMP_LEMMA = top_thm ();;

g `!f s z n m i.
     open s /\ f holomorphic_on s /\ (!w. w IN s ==> f w IN s) /\
     z IN s /\ f z = z /\ complex_derivative f z = Cx (&1) /\
     (!i. 1 < i /\ i <= n ==> higher_complex_derivative i f z = Cx (&0)) /\
     i <= n
     ==> higher_complex_derivative i (ITER m f) z =
         higher_complex_derivative i f z`;;
e (GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC);;
e (REWRITE_TAC [RIGHT_FORALL_IMP_THM; IMP_CONJ]);;
e (REWRITE_TAC [IMP_IMP]);;
e (STRIP_TAC);;
e (ASSERT_TAC `!m. ITER m f z = z:complex`);;
e (INDUCT_TAC THEN ASM_REWRITE_TAC [ITER]);;
e (ASSERT_TAC `!m (w:complex). w IN s ==> ITER m f w IN s`);;
e (INDUCT_TAC THEN ASM_SIMP_TAC [ITER]);;
e (ASSERT_TAC `!m. ITER m f holomorphic_on s`);;
e (INDUCT_TAC THEN REWRITE_TAC [ITER_POINTLESS]);;
e (ASM_SIMP_TAC [I_DEF; HOLOMORPHIC_ON_ID]);;
e (MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE);;
e (EXISTS_TAC `s:complex ->bool`);;
e (ASM_REWRITE_TAC []);;
e (INDUCT_TAC);;
e (REWRITE_TAC [ITER_POINTLESS; I_DEF; HIGHER_COMPLEX_DERIVATIVE_ID]);;
e (REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
   ASM_REWRITE_TAC [higher_complex_derivative]);;
e (REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
   ASM_REWRITE_TAC [higher_complex_derivative; ONE]);;
e (MATCH_MP_TAC EQ_SYM);;
e (FIRST_X_ASSUM MATCH_MP_TAC);;
e (ASM_SIMP_TAC [ARITH_RULE `~(i = 0) /\ ~(i = 1) ==> 1 < i`]);;
e (GEN_TAC THEN DISCH_TAC);;
e (REWRITE_TAC [ITER_ALT_POINTLESS]);;
e (TRANS_TAC `higher_complex_derivative i (ITER m f) (f z)`);;
e (MATCH_MP_TAC HIGHER_COMPLEX_DERIVATIVE_COMP_LEMMA);;
e (EXISTS_TAC `s:complex ->bool`);;
e (EXISTS_TAC `s:complex ->bool`);;
e (EXISTS_TAC `n:num`);;
e (ASM_REWRITE_TAC []);;
e (ASM_REWRITE_TAC []);;
e (FIRST_X_ASSUM MATCH_MP_TAC);;
e (ASM_REWRITE_TAC []);;
let HIGHER_COMPLEX_DERIVATIVE_COMP_ITER_LEMMA = top_thm ();;

g `!f s z n m.
     open s /\ f holomorphic_on s /\ (!w. w IN s ==> f w IN s) /\
     z IN s /\ f z = z /\ complex_derivative f z = Cx (&1) /\
     (!i. 1 < i /\ i < n ==> higher_complex_derivative i f z = Cx (&0)) /\
     1 < n
     ==> higher_complex_derivative n (ITER m f) z =
         Cx(&m) * higher_complex_derivative n f z`;;
e (GEN_TAC THEN GEN_TAC THEN GEN_TAC);;
e (INDUCT_TAC THEN REWRITE_TAC [LT_SUC_LE] THEN REWRITE_TAC [LT]);;
e (REWRITE_TAC [RIGHT_FORALL_IMP_THM]);;
e (STRIP_TAC);;
e (ASSERT_TAC `!m. ITER m f z = z:complex`);;
e (INDUCT_TAC THEN ASM_REWRITE_TAC [ITER]);;
e (ASSERT_TAC `!m (w:complex). w IN s ==> ITER m f w IN s`);;
e (INDUCT_TAC THEN ASM_SIMP_TAC [ITER]);;
e (ASSERT_TAC `!m. ITER m f holomorphic_on s`);;
e (INDUCT_TAC THEN REWRITE_TAC [ITER_POINTLESS]);;
e (ASM_SIMP_TAC [I_DEF; HOLOMORPHIC_ON_ID]);;
e (MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE);;
e (EXISTS_TAC `s:complex ->bool`);;
e (ASM_REWRITE_TAC []);;
e (ASSERT_TAC `!w. w IN s ==> f complex_differentiable at w`);;
e (ASM_MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;
e (ASSERT_TAC `!m w. w IN s ==> ITER m f complex_differentiable at w`);;
e (ASM_MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;
e (ASSERT_TAC `!m. complex_derivative (ITER m f) z = Cx(&1)`);;
e (INDUCT_TAC THEN ASM_REWRITE_TAC [ITER_POINTLESS]);;
e (REWRITE_TAC [I_DEF; COMPLEX_DERIVATIVE_ID]);;
e (ASM_SIMP_TAC [COMPLEX_DERIVATIVE_CHAIN; HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;
e (REWRITE_TAC [COMPLEX_MUL_LID]);;

e (INDUCT_TAC THEN
   REWRITE_TAC [higher_complex_derivative_alt; ITER_POINTLESS]);;
e (ASM_REWRITE_TAC [COMPLEX_MUL_LZERO; I_DEF; COMPLEX_DERIVATIVE_ID;
                    HIGHER_COMPLEX_DERIVATIVE_CONST;
		    ARITH_RULE `n = 0 <=> ~(1 <= n)`]);;
e (TRANS_TAC `higher_complex_derivative n
              (\w. complex_derivative f (ITER m f w) * complex_derivative (ITER m f) w) z`);;
e (MATCH_MP_TAC HIGHER_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN);;
e (EXISTS_TAC `s:complex->bool`);;
e (ASM_REWRITE_TAC[]);;
e CONJ_TAC;;

e (REWRITE_TAC [o_DEF]);;
e (MATCH_MP_TAC HOLOMORPHIC_COMPLEX_DERIVATIVE);;
e (ASM_REWRITE_TAC []);;
e (ONCE_REWRITE_TAC [GSYM o_DEF]);;
e (MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE);;
e (EXISTS_TAC `s:complex->bool`);;
e (ASM_REWRITE_TAC [ETA_AX]);;

e CONJ_TAC;;
e (MATCH_MP_TAC HOLOMORPHIC_ON_MUL);;
e CONJ_TAC;;
e (ONCE_REWRITE_TAC [GSYM o_DEF]);;
e (MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE);;
e (EXISTS_TAC `s:complex->bool`);;
e (ASM_REWRITE_TAC[ETA_AX]);;
e (MATCH_MP_TAC HOLOMORPHIC_COMPLEX_DERIVATIVE);;
e (ASM_REWRITE_TAC[]);;
e (ONCE_REWRITE_TAC [GSYM o_DEF]);;
e (MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE);;
e (EXISTS_TAC `s:complex->bool`);;
e (ASM_REWRITE_TAC[HOLOMORPHIC_ON_ID]);;
e (MATCH_MP_TAC HOLOMORPHIC_COMPLEX_DERIVATIVE);;
e (ASM_REWRITE_TAC[]);;

e (GEN_TAC THEN DISCH_TAC);;
e (MATCH_MP_TAC COMPLEX_DERIVATIVE_CHAIN);;
e CONJ_TAC;;
e (MATCH_MP_TAC HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT);;
e (ASM_MESON_TAC []);;

e (MATCH_MP_TAC HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT);;
e (ASM_MESON_TAC []);;

e (TRANS_TAC
    `vsum (0..n)
       (\i. Cx (&(binom (n,i))) *
            higher_complex_derivative i (\w. complex_derivative f (ITER m f w)) z *
            higher_complex_derivative (n - i) (complex_derivative (ITER m f)) z)`);;
e (MATCH_MP_TAC HIGHER_COMPLEX_DERIVATIVE_MUL);;
e (EXISTS_TAC `s:complex->bool`);;
e (ASM_REWRITE_TAC[]);;
e CONJ_TAC;;
e (ONCE_REWRITE_TAC [GSYM o_DEF]);;
e (MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE);;
e (EXISTS_TAC `s:complex->bool`);;
e (ASM_REWRITE_TAC[ETA_AX]);;
e (MATCH_MP_TAC HOLOMORPHIC_COMPLEX_DERIVATIVE);;
e (ASM_REWRITE_TAC[]);;
e (MATCH_MP_TAC HOLOMORPHIC_COMPLEX_DERIVATIVE);;
e (ASM_REWRITE_TAC[]);;

e (TRANS_TAC
    `vsum {0,n}
       (\i. Cx (&(binom (n,i))) *
            higher_complex_derivative i (\w. complex_derivative f (ITER m f w)) z *
            higher_complex_derivative (n - i) (complex_derivative (ITER m f)) z)`);;
e (MATCH_MP_TAC VSUM_SUPERSET);;

e (REWRITE_TAC [INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG_0; LE_0; LE_REFL;
                IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM]);;

e (X_GEN_TAC `i:num`);;
e (STRIP_TAC);;
e (REWRITE_TAC [GSYM higher_complex_derivative_alt]);;
e (ASSERT_TAC `1 < SUC (n-i) /\ SUC (n-i) <= n`);;
e (ASM_SIMP_TAC [ARITH_RULE `i <= n /\ ~(i=0) /\ ~(i=n)
                             ==> 1 < SUC (n-i) /\ SUC (n-i) <= n`]);;
e (ASM_SIMP_TAC []);;

e (SUBGOAL_THEN
     `higher_complex_derivative (SUC (n - i)) (ITER m f) z = Cx(&0)`
     SUBST1_TAC);;
e (TRANS_TAC `higher_complex_derivative (SUC (n - i)) f z`);;
e (MATCH_MP_TAC HIGHER_COMPLEX_DERIVATIVE_COMP_ITER_LEMMA);;
e (EXISTS_TAC `s:complex->bool`);;
e (ASM_REWRITE_TAC []);;
e (EXISTS_TAC `n:num`);;
e (ASM_REWRITE_TAC []);;
e (FIRST_X_ASSUM MATCH_MP_TAC);;
e (ASM_REWRITE_TAC []);;
e (ASM_REWRITE_TAC [COMPLEX_MUL_RZERO; COMPLEX_VEC_0]);;
e (SIMP_TAC [VSUM_CLAUSES; FINITE_RULES; IN_INSERT; NOT_IN_EMPTY]);;
e (REWRITE_TAC [binom; BINOM_REFL; COMPLEX_MUL_LID; SUB_REFL; SUB; higher_complex_derivative]);;
e (ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC []);;
e (REWRITE_TAC [higher_complex_derivative]);;
e (POP_ASSUM SUBST_ALL_TAC);;
e (RULE_ASSUM_TAC (REWRITE_RULE [higher_complex_derivative]));;
e (ASM_REWRITE_TAC [COMPLEX_MUL_RID; COMPLEX_MUL_LID; COMPLEX_VEC_0; COMPLEX_ADD_RID]);;
e (ASM_MESON_TAC [ARITH_RULE `~(1 <= 0)`]);;
(***KILLME*** !!!!!!!!!!!!!!!!!!!!!!!!!!!! *)

e (ASM_REWRITE_TAC [COMPLEX_MUL_LID; COMPLEX_VEC_0; COMPLEX_ADD_RID]);;
e (ASM_REWRITE_TAC [COMPLEX_MUL_RID]);;
e (ASM_REWRITE_TAC [GSYM higher_complex_derivative_alt]);;
e (SUBGOAL_THEN
     `(\w. complex_derivative f (ITER m f w)) = complex_derivative f o ITER m f`
     SUBST1_TAC);;
e (REWRITE_TAC [FUN_EQ_THM; o_THM]);;
e (SUBGOAL_THEN
     `higher_complex_derivative n (complex_derivative f o ITER m f) z =
      higher_complex_derivative n (complex_derivative f) (ITER m f z)`
     SUBST1_TAC);;
e (MATCH_MP_TAC HIGHER_COMPLEX_DERIVATIVE_COMP_LEMMA);;
e (EXISTS_TAC `s:complex->bool`);;
e (EXISTS_TAC `s:complex->bool`);;
e (EXISTS_TAC `n:num`);;
e (ASM_REWRITE_TAC[]);;
e (ASM_SIMP_TAC[HOLOMORPHIC_COMPLEX_DERIVATIVE; LE_REFL]);;
e (REPEAT STRIP_TAC);;
e (TRANS_TAC `higher_complex_derivative i f z`);;
e (MATCH_MP_TAC HIGHER_COMPLEX_DERIVATIVE_COMP_ITER_LEMMA);;
e (EXISTS_TAC `s:complex->bool`);;
e (EXISTS_TAC `n:num`);;
e (ASM_REWRITE_TAC[]);;
e (ASM_SIMP_TAC[]);;
e (ASSERT_TAC `Cx (&(SUC m)) = Cx (&m) +  Cx (&1)`);;
r 1;;
e (ASM_REWRITE_TAC [COMPLEX_POLY_CLAUSES; GSYM higher_complex_derivative_alt]);;
e (REWRITE_TAC [GSYM CX_ADD; REAL_OF_NUM_ADD; ONE; ADD_SUC; ADD_0]);;
let HIGHER_COMPLEX_DERIVATIVE_ITER_TOP_LEMMA = top_thm ();;

(********************************************************************)
g `!f z y r B0 n.
     &0 < r /\ 0 < n /\ f holomorphic_on ball(z,r) /\ f continuous_on cball(z,r) /\
     (!w. w IN ball(z,r) ==> f w IN ball(y,B0))
     ==> norm (higher_complex_derivative n f z) <= &(FACT n) * B0 / r pow n`;;
e (REPEAT STRIP_TAC);;
(** Le derivate non cambiano aggiungendo una costante **)
e (SUBGOAL_THEN `higher_complex_derivative n f z =
                 higher_complex_derivative n (\w. f w - y) z`
     SUBST1_TAC);;
e (TRANS_TAC `higher_complex_derivative n (\w. f w) z -
              higher_complex_derivative n (\w. y) z`);;
e (ASM_SIMP_TAC
   [HIGHER_COMPLEX_DERIVATIVE_CONST; ARITH_RULE `0<n ==> ~(n=0)`]);;
e (REWRITE_TAC [COMPLEX_SUB_RZERO; ETA_AX]);;
e (MATCH_MP_TAC EQ_SYM);;
e (REWRITE_TAC [ETA_AX]);;
e (MATCH_MP_TAC HIGHER_COMPLEX_DERIVATIVE_SUB);;
e (EXISTS_TAC `ball(z:complex,r)`);;
e (ASM_SIMP_TAC [OPEN_BALL; HOLOMORPHIC_ON_CONST; CENTRE_IN_BALL]);;
(** Riconduciamoci a un "multiplo" del goal **)
e(SUBGOAL_THEN
  `norm ((Cx (&2) * Cx pi * ii) / Cx (&(FACT n)) 
         * higher_complex_derivative n (\w. f w - y) z)
   <= (B0 / r pow (n + 1)) * &2 * pi * r` MP_TAC);;
e(MATCH_MP_TAC HAS_PATH_INTEGRAL_BOUND_CIRCLEPATH);;
e(EXISTS_TAC `(\u. (f u - y) / (u - z) pow (n + 1))`);;
e(EXISTS_TAC `z:complex`);;
e(STRIP_TAC);;
e(MATCH_MP_TAC CAUCHY_HAS_PATH_INTEGRAL_HIGHER_DERIVATIVE_CIRCLEPATH);;
e(ASM_SIMP_TAC[CENTRE_IN_BALL]);;
e(CONJ_TAC);;
e(MATCH_MP_TAC CONTINUOUS_ON_SUB);;
e(ASM_REWRITE_TAC [CONTINUOUS_ON_CONST]);;
e(MATCH_MP_TAC HOLOMORPHIC_ON_SUB);;
e(ASM_REWRITE_TAC [HOLOMORPHIC_ON_CONST]);;
e(ASM_SIMP_TAC[]);;
e(STRIP_TAC);;
e(MATCH_MP_TAC REAL_LE_DIV);;
e(STRIP_TAC);;
e(MATCH_MP_TAC REAL_LT_IMP_LE);;
e(MATCH_MP_TAC (prove(`(?x. &0 <= x /\ x < B0) ==> &0 < B0`, REAL_ARITH_TAC)));;
e(EXISTS_TAC `norm ((\u. (f:complex->complex) u - y) z)`);;
e(SIMP_TAC[NORM_POS_LE]);;
e (SUBGOAL_THEN 
   `!w:complex. f w IN ball(y,B0) ==> norm (f w - y) < B0` 
   MATCH_MP_TAC);;
e (ASM_MESON_TAC [dist; DIST_SYM; IN_BALL; CENTRE_IN_BALL]);;
e(FIRST_ASSUM MATCH_MP_TAC);;
e(ASM_SIMP_TAC[CENTRE_IN_BALL]);;
e(MATCH_MP_TAC(SPECL [`r:real`;`n + 1`] REAL_POW_LE));;
e(ASM_SIMP_TAC[REAL_LT_IMP_LE]);;
e(REPEAT STRIP_TAC);;
e(ASM_REWRITE_TAC[COMPLEX_NORM_DIV;COMPLEX_NORM_POW]);;
e(ASM_SIMP_TAC [REAL_LE_DIV2_EQ; REAL_POW_LT]);;
e(ONCE_REWRITE_TAC[MESON[] `!(f:complex->complex). 
  (f x - y) = (\w. f w - y) x`]);;
e(MATCH_MP_TAC CONTINUOUS_ON_CLOSURE_LE);;
e(EXISTS_TAC `ball(z:complex,r)`);;
e(ASM_SIMP_TAC[CLOSURE_BALL]);;
e(REPEAT STRIP_TAC);;
e(MATCH_MP_TAC CONTINUOUS_ON_SUB);;
e(ASM_SIMP_TAC[CONTINUOUS_ON_CONST]);;
e (SUBGOAL_THEN 
   `!w:complex. f w IN ball(y,B0) ==> norm (f w - y) <= B0` 
   MATCH_MP_TAC);;
e(REWRITE_TAC[GSYM dist;IN_BALL;DIST_SYM;REAL_LT_IMP_LE]);;
e(ASM_MESON_TAC [dist; DIST_SYM; IN_BALL; CENTRE_IN_BALL]);;
e(ASM_REWRITE_TAC[cball;IN_ELIM_THM;dist;DIST_SYM]);;
e(ASM_SIMP_TAC[REAL_EQ_IMP_LE]);;
(** Riscrittura semplificatrice di norme complesse **)
e (REWRITE_TAC [COMPLEX_NORM_MUL; COMPLEX_NORM_DIV; COMPLEX_NORM_II;
                COMPLEX_NORM_CX; REAL_ABS_NUM; REAL_ABS_PI;
		REAL_MUL_RID]);;
e (STRIP_TAC);;
(** Introduzione di a, e dimostrazione che &0<a **)
e (ABBREV_TAC `a = (&2 * pi) / &(FACT n)`);;
e (SUBGOAL_THEN `&0 < a` ASSUME_TAC);;
e (EXPAND_TAC "a");;
e (SIMP_TAC [REAL_LT_DIV; REAL_LT_MUL; REAL_OF_NUM_LT; FACT_LT; ARITH; PI_POS]);;
(** Altra uguaglianza algebrica **)
e (SUBGOAL_THEN 
   `B0 / r pow (n + 1) * &2 * pi * r = a * (&(FACT n) * B0 / r pow n)` 
   SUBST_ALL_TAC);;
e (EXPAND_TAC "a");;
e (REWRITE_TAC [GSYM ADD1; real_pow]);;
e (SUBGOAL_THEN `~(&(FACT n) = &0) /\ &0 < r` MP_TAC);;
e (ASM_REWRITE_TAC[FACT_NZ; REAL_OF_NUM_EQ]);;
e (CONV_TAC REAL_FIELD);;
(** Cancelliamo a **)
e (ASM_MESON_TAC [REAL_LE_LCANCEL_IMP]);;
let CAUCHY_HIGHER_COMPLEX_DERIVATIVE_BOUND = top_thm ();;

g `!f z r n m w.
     f holomorphic_on ball(z,r) /\ f continuous_on cball(z,r) /\
     &0 < r /\ f z = z /\ 
     (!w. w IN ball(z,r) ==> f w IN ball(z,r)) /\
     (!w. w IN cball(z,r) ==> f w IN cball(z,r)) /\
     complex_derivative f z = Cx (&1) /\ w IN ball(z,r)
     ==> f w = w`;;
e (REWRITE_TAC [RIGHT_FORALL_IMP_THM; IMP_CONJ]);;
e (REPEAT GEN_TAC);;
e (REPEAT DISCH_TAC);;

e (ASSERT_TAC `!m (w:complex). w IN ball(z,r)
                               ==> ITER m f w IN ball(z,r)` THENL
   [INDUCT_TAC THEN ASM_SIMP_TAC [ITER]; ALL_TAC]);;

e (ASSERT_TAC `!m (w:complex). w IN cball(z,r)
                               ==> ITER m f w IN cball(z,r)` THENL
   [INDUCT_TAC THEN ASM_SIMP_TAC [ITER]; ALL_TAC]);;

e (ASSERT_TAC `!m. ITER m f holomorphic_on ball(z,r)` THENL
   [INDUCT_TAC THEN REWRITE_TAC [ITER_POINTLESS] THEN
    ASM_SIMP_TAC [I_DEF; HOLOMORPHIC_ON_ID];
    ALL_TAC]);;

e (MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE);;
e (EXISTS_TAC `ball(z:complex,r)`);;
e (ASM_REWRITE_TAC []);;

e (ASSERT_TAC `!m. ITER m f continuous_on cball(z:complex,r)`);;
e (INDUCT_TAC THEN REWRITE_TAC [ITER_POINTLESS]);;
e (ASM_SIMP_TAC [I_DEF; CONTINUOUS_ON_ID]);;

e (MATCH_MP_TAC CONTINUOUS_ON_COMPOSE);;
e (ASM_REWRITE_TAC []);;
e (MATCH_MP_TAC CONTINUOUS_ON_SUBSET);;
e (EXISTS_TAC `cball(z:complex,r)`);;
e (ASM_REWRITE_TAC [SUBSET; IN_IMAGE]);;
e (REPEAT STRIP_TAC THEN ASM_SIMP_TAC []);;

e (REPEAT STRIP_TAC THEN TRANS_TAC `I w:complex` THENL
   [MATCH_MP_TAC HOLOMORPHIC_FUN_EQ_ON_BALL; REWRITE_TAC [I_DEF]]);;
e (EXISTS_TAC `z:complex`);;
e (EXISTS_TAC `r:real`);;
e (ASM_REWRITE_TAC [I_DEF; HOLOMORPHIC_ON_ID]);;
e (GEN_TAC);;
e (STRIP_ASSUME_TAC (ARITH_RULE `n = 0 \/ n = 1 \/ 1 < n`));;
e (ASM_REWRITE_TAC [higher_complex_derivative]);;
e (ASM_REWRITE_TAC [ONE; higher_complex_derivative; COMPLEX_DERIVATIVE_ID]);;
e (ASM_REWRITE_TAC [HIGHER_COMPLEX_DERIVATIVE_ID]);;
e (ASM_SIMP_TAC [ARITH_RULE `1 < n ==> ~(n=0) /\ ~(n=1)`]);;
e (POP_ASSUM MP_TAC);;
e (SPEC_TAC (`n:num`,`n:num`));;
e (MATCH_MP_TAC num_WF);;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC [GSYM COMPLEX_NORM_ZERO]);;
e (MATCH_MP_TAC REAL_ARCH_RDIV_EQ_0);;
e (REWRITE_TAC [NORM_POS_LE]);;
e (EXISTS_TAC `&(FACT n) * r / r pow n`);;
e (CONJ_TAC);;
e (MATCH_MP_TAC REAL_LE_MUL);;
e (CONJ_TAC);;
e (MATCH_MP_TAC REAL_LT_IMP_LE);;
e (MATCH_MP_TAC REAL_LTE_TRANS);;
e (EXISTS_TAC `&1`);;
e (REWRITE_TAC [REAL_LT_01; FACT_LE; REAL_OF_NUM_LE]);;
e (MATCH_MP_TAC REAL_LE_DIV);;
e (ASM_SIMP_TAC [REAL_LT_IMP_LE]);;
e (ASM_SIMP_TAC [REAL_LT_IMP_LE; REAL_POW_LE]);;
e (REPEAT STRIP_TAC);;
e (ONCE_REWRITE_TAC [GSYM COMPLEX_NORM_NUM]);;
e (REWRITE_TAC [GSYM COMPLEX_NORM_MUL]);;
e (SUBGOAL_THEN
      `Cx(&m) * higher_complex_derivative n f z =
       higher_complex_derivative n (ITER m f) z`
     SUBST1_TAC);;
e (MATCH_MP_TAC (GSYM HIGHER_COMPLEX_DERIVATIVE_ITER_TOP_LEMMA));;
e (EXISTS_TAC `ball (z:complex,r)`);;
e (ASM_SIMP_TAC [OPEN_BALL; CENTRE_IN_BALL]);;
e (REWRITE_TAC [COMPLEX_NORM_CX]);;
e (SUBGOAL_THEN `abs (&(FACT n)) = &(FACT n)` SUBST1_TAC);;
e (REWRITE_TAC [REAL_ABS_REFL]);;

e (MATCH_MP_TAC REAL_LT_IMP_LE);;
e (MATCH_MP_TAC REAL_LTE_TRANS);;
e (EXISTS_TAC `&1`);;
e (REWRITE_TAC [REAL_LT_01; FACT_LE; REAL_OF_NUM_LE]);;

e (MATCH_MP_TAC CAUCHY_HIGHER_COMPLEX_DERIVATIVE_BOUND);;
e (EXISTS_TAC `z:complex`);;
e (ASM_SIMP_TAC [ARITH_RULE `1<n ==> 0 < n`]);;
let FIRST_CARTAN_THEOREM = top_thm ();;