text_formalization/tame/ssreflect/tame_lemmas-compiled.hl

   1 flyspeck_needs "../formal_lp/hypermap/ssreflect/add_triangle-compiled.hl";;
   2
   3 (* Module Tame_lemmas*)
   4 module Tame_lemmas = struct
   5
   6 let reflection = new_definition `reflection n x = x - (&2 * (x dot n) / (n dot n)) % n`;;
   7 let kcblrqc_ineq_tml =
   8   let has_id = (fun t -> not(intersect ["KCBLRQC"] (Ineq.flypaper_ids t) = [])) in
   9   let extra_ids = [
  10         "3287695934";
  11         "6988401556";
  12         "3862621143 back";
  13         "3862621143 front";
  14         "3862621143 side";
  15         "4240815464 a reduced";
  16         "6944699408 a reduced";
  17         "7043724150 a reduced v2";
  18   ] in
  19   let idl = (filter (fun t -> has_id t or mem t.idv extra_ids) !Ineq.ineqs) in
  20   let tml = map (fun t -> t.ineq) idl in
  21     end_itlist (curry mk_conj) tml;;
  22 let kcblrqc_ineq_def = new_definition
  23         (mk_eq (`kcblrqc_ineq_def:bool`, kcblrqc_ineq_tml));;
  24 open Tame_general;;
  25 open Add_triangle;;
  26 open Fan_defs;;
  27 open Pack_defs;;
  28 open Hypermap;;
  29 open Hypermap_and_fan;;
  30 open Hypermap_iso;;
  31 open Ssrbool;;
  32 open Ssrnat;;
  33
  34 (* Section Reflection *)
  35 Sections.begin_section "Reflection";;
  36 let VECTOR_MUL_RZERO = GEN_ALL VECTOR_MUL_RZERO;;
  37 let VECTOR_SUB_RZERO = GEN_ALL VECTOR_SUB_RZERO;;
  38 let VECTOR_SUB_RDISTRIB = GEN_ALL VECTOR_SUB_RDISTRIB;;
  39 let VECTOR_ADD_RDISTRIB = GEN_ALL VECTOR_ADD_RDISTRIB;;
  40 let VECTOR_SUB_LDISTRIB = GEN_ALL VECTOR_SUB_LDISTRIB;;
  41 (Sections.add_section_type (mk_var ("x", (`:real^N`))); Sections.add_section_type (mk_var ("y", (`:real^N`))); Sections.add_section_type (mk_var ("d", (`:real^N`))));;
  42
  43 (* Lemma reflection_at0 *)
  44 let reflection_at0 = Sections.section_proof ["x"]
  45 `reflection (vec 0) x = x`
  46 [
  47    (((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("VECTOR_MUL_RZERO", [VECTOR_MUL_RZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("VECTOR_SUB_RZERO", [VECTOR_SUB_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  48 ];;
  49
  50 (* Lemma reflection_eq *)
  51 let reflection_eq = Sections.section_proof ["n";"x"]
  52 `x dot n = &0 ==> reflection n x = x`
  53 [
  54    ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
  55    (((((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_LZERO", [REAL_MUL_LZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_RZERO", [REAL_MUL_RZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("VECTOR_MUL_LZERO", [VECTOR_MUL_LZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("VECTOR_SUB_RZERO", [VECTOR_SUB_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  56 ];;
  57
  58 (* Lemma reflection_eq2 *)
  59 let reflection_eq2 = Sections.section_proof ["n";"x"]
  60 `reflection n x = x <=> x dot n = &0`
  61 [
  62    ((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`n = vec 0`))) (disch_eq_tac "n0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) (((((use_arg_then2 ("n0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("reflection_at0", [reflection_at0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_RZERO", [DOT_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
  63    ((THENL_LAST) (split_tac) (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("reflection_eq", [reflection_eq])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (done_tac)));
  64    ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (VECTOR_ARITH `!x y. x - y = x <=> y = vec 0`)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("VECTOR_MUL_EQ_0", [VECTOR_MUL_EQ_0]))(thm_tac (new_rewrite [] [])))));
  65    (((((use_arg_then2 ("n0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orbF", [orbF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_INV_EQ_0", [REAL_INV_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_EQ_0", [DOT_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n0", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
  66 ];;
  67
  68 (* Lemma reflection0 *)
  69 let reflection0 = Sections.section_proof ["n"]
  70 `reflection n (vec 0) = vec 0`
  71 [
  72    (((((use_arg_then2 ("reflection_eq", [reflection_eq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("DOT_LZERO", [DOT_LZERO]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  73 ];;
  74
  75 (* Lemma reflection_sub *)
  76 let reflection_sub = Sections.section_proof ["n";"x";"y"]
  77 `reflection n (x - y) = reflection n x - reflection n y`
  78 [
  79    ((repeat_tactic 1 9 (((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("DOT_LSUB", [DOT_LSUB]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_ASSOC", [REAL_MUL_ASSOC]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_SUB_LDISTRIB", [REAL_SUB_LDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_SUB_RDISTRIB", [REAL_SUB_RDISTRIB]))(thm_tac (new_rewrite [] [])))));
  80    ((((use_arg_then2 ("VECTOR_SUB_RDISTRIB", [VECTOR_SUB_RDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (VECTOR_ARITH_TAC) THEN (done_tac));
  81 ];;
  82
  83 (* Lemma reflection_add *)
  84 let reflection_add = Sections.section_proof ["n";"x";"y"]
  85 `reflection n (x + y) = reflection n x + reflection n y`
  86 [
  87    ((repeat_tactic 1 9 (((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("DOT_LADD", [DOT_LADD]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_ASSOC", [REAL_MUL_ASSOC]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_ADD_LDISTRIB", [REAL_ADD_LDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_RDISTRIB", [REAL_ADD_RDISTRIB]))(thm_tac (new_rewrite [] [])))));
  88    ((((use_arg_then2 ("VECTOR_ADD_RDISTRIB", [VECTOR_ADD_RDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (VECTOR_ARITH_TAC) THEN (done_tac));
  89 ];;
  90
  91 (* Lemma reflection_cmul *)
  92 let reflection_cmul = Sections.section_proof ["n";"c";"x"]
  93 `reflection n (c % x) = c % reflection n x`
  94 [
  95    ((repeat_tactic 1 9 (((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("DOT_LMUL", [DOT_LMUL]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("VECTOR_SUB_LDISTRIB", [VECTOR_SUB_LDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("VECTOR_MUL_ASSOC", [VECTOR_MUL_ASSOC]))(thm_tac (new_rewrite [] [])))));
  96    (((repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_ASSOC", [REAL_MUL_ASSOC]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("REAL_MUL_SYM", [REAL_MUL_SYM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  97 ];;
  98
  99 (* Lemma norm_reflection *)
 100 let norm_reflection = Sections.section_proof ["n";"x"]
 101 `norm (reflection n x) = norm x`
 102 [
 103    ((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`n = vec 0`))) (disch_eq_tac "n0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) (((((use_arg_then2 ("n0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("reflection_at0", [reflection_at0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 104    ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NORM_EQ", [NORM_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_LSUB", [DOT_LSUB]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DOT_RSUB", [DOT_RSUB]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DOT_RMUL", [DOT_RMUL]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DOT_LMUL", [DOT_LMUL]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("DOT_SYM", [DOT_SYM])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
 105    ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`~(n dot n = &0)`))) (term_tac (have_gen_tac []ALL_TAC)))) ((CONV_TAC REAL_FIELD) THEN (done_tac)));
 106    ((((use_arg_then2 ("DOT_EQ_0", [DOT_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 107 ];;
 108
 109 (* Lemma dist_reflection *)
 110 let dist_reflection = Sections.section_proof ["n";"x";"y"]
 111 `dist (reflection n x, reflection n y) = dist (x, y)`
 112 [
 113    (((repeat_tactic 1 9 (((use_arg_then2 ("dist", [dist]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("reflection_sub", [reflection_sub]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("norm_reflection", [norm_reflection]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 114 ];;
 115
 116 (* Lemma dist_reflection_special *)
 117 let dist_reflection_special = Sections.section_proof ["n";"x";"y"]
 118 `y dot n = &0 ==> dist (reflection n x, y) = dist (x, y)`
 119 [
 120    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("reflection_eq", [reflection_eq])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [1] [])))))) THEN (((use_arg_then2 ("dist_reflection", [dist_reflection]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 121 ];;
 122
 123 (* Lemma reflection_dot *)
 124 let reflection_dot = Sections.section_proof ["n";"x"]
 125 `(reflection n x) dot n = --(x dot n)`
 126 [
 127    ((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`n = vec 0`))) (disch_eq_tac "n0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) (((((use_arg_then2 ("n0", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DOT_RZERO", [DOT_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_NEG_0", [REAL_NEG_0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 128    ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_LSUB", [DOT_LSUB]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_LMUL", [DOT_LMUL]))(thm_tac (new_rewrite [] [])))));
 129    ((((use_arg_then2 ("n0", [])) (disch_tac [])) THEN (clear_assumption "n0") THEN BETA_TAC) THEN (((use_arg_then2 ("DOT_EQ_0", [DOT_EQ_0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (CONV_TAC REAL_FIELD) THEN (done_tac));
 130 ];;
 131
 132 (* Lemma dist_reflection_lemma *)
 133 let dist_reflection_lemma = Sections.section_proof ["n";"x";"y"]
 134 `dist (reflection n x, y) pow 2
 135         = dist (x, y) pow 2 + &4 * ((y dot n) * (x dot n)) / (n dot n)`
 136 [
 137    (((fun arg_tac -> arg_tac (Arg_term (`n = vec 0`))) (disch_eq_tac "n0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
 138    (((((use_arg_then2 ("n0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("reflection_at0", [reflection_at0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_RZERO", [DOT_RZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_LZERO", [REAL_MUL_LZERO]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_MUL_RZERO", [REAL_MUL_RZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_RID", [REAL_ADD_RID]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 139    (((use_arg_then2 ("Collect_geom.DIST_POW2_DOT", [Collect_geom.DIST_POW2_DOT]))(thm_tac (new_rewrite [] []))));
 140    ((fun arg_tac -> arg_tac (Arg_term (`y = reflection n y + (&2 * (y dot n) / (n dot n)) % n`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [1; 2] [])))))));
 141    ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (VECTOR_ARITH_TAC) THEN (done_tac));
 142    ((fun arg_tac -> arg_tac (Arg_term (`&2 * _`))) (term_tac (set_tac "a")));
 143    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`b - (c + d) = (b - c) - d:real^N`))) (term_tac (have_gen_tac ["b"; "c"; "d"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((VECTOR_ARITH_TAC) THEN (done_tac)));
 144    ((fun arg_tac -> arg_tac (Arg_term (`(b - c) dot (b - c) = b dot b + c dot c - &2 * (b dot c:real^N)`))) (term_tac (have_gen_tac ["b"; "c"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
 145    (((((use_arg_then2 ("DOT_LSUB", [DOT_LSUB]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DOT_RSUB", [DOT_RSUB]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("DOT_SYM", [DOT_SYM])) (fun fst_arg -> (use_arg_then2 ("b", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("c", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (VECTOR_ARITH_TAC) THEN (done_tac));
 146    ((((use_arg_then2 ("Collect_geom.DIST_POW2_DOT", [Collect_geom.DIST_POW2_DOT]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dist_reflection", [dist_reflection]))(thm_tac (new_rewrite [] [])))));
 147    ((((use_arg_then2 ("DOT_LSUB", [DOT_LSUB]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_LMUL", [DOT_LMUL]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DOT_RMUL", [DOT_RMUL]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("reflection_dot", [reflection_dot]))(thm_tac (new_rewrite [] []))))));
 148    ((((use_arg_then2 ("a_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("n0", [])) (disch_tac [])) THEN (clear_assumption "n0") THEN BETA_TAC) THEN (((use_arg_then2 ("DOT_EQ_0", [DOT_EQ_0]))(gsym_then (thm_tac (new_rewrite [] []))))));
 149    ((CONV_TAC REAL_FIELD) THEN (done_tac));
 150 ];;
 151
 152 (* Finalization of the section Reflection *)
 153 let reflection_at0 = Sections.finalize_theorem reflection_at0;;
 154 let reflection_eq = Sections.finalize_theorem reflection_eq;;
 155 let reflection_eq2 = Sections.finalize_theorem reflection_eq2;;
 156 let reflection0 = Sections.finalize_theorem reflection0;;
 157 let reflection_sub = Sections.finalize_theorem reflection_sub;;
 158 let reflection_add = Sections.finalize_theorem reflection_add;;
 159 let reflection_cmul = Sections.finalize_theorem reflection_cmul;;
 160 let norm_reflection = Sections.finalize_theorem norm_reflection;;
 161 let dist_reflection = Sections.finalize_theorem dist_reflection;;
 162 let dist_reflection_special = Sections.finalize_theorem dist_reflection_special;;
 163 let reflection_dot = Sections.finalize_theorem reflection_dot;;
 164 let dist_reflection_lemma = Sections.finalize_theorem dist_reflection_lemma;;
 165 Sections.end_section "Reflection";;
 166
 167 (* Section Misc *)
 168 Sections.begin_section "Misc";;
 169 (Sections.add_section_type (mk_var ("v", (`:real^3`))));;
 170
 171 (* Lemma delta_y_pos *)
 172 let delta_y_pos = Sections.section_proof ["v";"w";"w'"]
 173 `let y1 = norm v in
 174          let y2 = norm w in
 175          let y3 = norm w' in
 176          let y4 = dist (w,w') in
 177          let y5 = dist (v,w') in
 178          let y6 = dist (v,w) in
 179                 &0 <= delta_y y1 y2 y3 y4 y5 y6`
 180 [
 181    (repeat_tactic 1 9 ((CONV_TAC let_CONV)));
 182    ((((use_arg_then2 ("Sphere.delta_y", [Sphere.delta_y]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DELTA_EQ_DELTA_X", [DELTA_EQ_DELTA_X]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DIST_0", [DIST_0]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] [])))))));
 183    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Collect_geom.DELTA_POS_4POINTS", [Collect_geom.DELTA_POS_4POINTS])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0:real^3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 184    ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 185 ];;
 186
 187 (* Lemma quadratic_root_plus_works *)
 188 let quadratic_root_plus_works = Sections.section_proof ["a";"b";"c"]
 189 `~(a = &0) /\ &0 <= b pow 2 - &4 * a * c ==>
 190         let x = quadratic_root_plus (a,b,c) in
 191                 a * x pow 2 + b * x + c = &0`
 192 [
 193    ((BETA_TAC THEN (move ["ineqs"])) THEN (CONV_TAC let_CONV));
 194    (((fun arg_tac -> (use_arg_then2 ("Collect_geom2.FACTOR_OF_QUADRARTIC", [Collect_geom2.FACTOR_OF_QUADRARTIC])) (fun fst_arg -> (use_arg_then2 ("ineqs", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))));
 195    ((((use_arg_then2 ("Sphere.quadratic_root_plus", [Sphere.quadratic_root_plus]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 196 ];;
 197
 198 (* Lemma quadratic_root_plus_eq *)
 199 let quadratic_root_plus_eq = Sections.section_proof ["a";"b";"c";"x"]
 200 `&0 < a /\ &0 <= b pow 2 - &4 * a * c
 201         /\ &0 <= b /\ (a * x pow 2 + b * x + c = &0) /\ &0 <= x
 202         ==> quadratic_root_plus (a,b,c) = x`
 203 [
 204    (BETA_TAC THEN (case THEN (move ["a_gt0"])) THEN (case THEN (move ["disc_ge0"])) THEN (case THEN (move ["b_ge0"])) THEN (case THEN (move ["x_root"])) THEN (move ["x_ge0"]));
 205    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(a = &0)`))) (term_tac (have_gen_tac [](move ["a_neq"])))) ((((use_arg_then2 ("a_gt0", [])) (disch_tac [])) THEN (clear_assumption "a_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
 206    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Collect_geom2.FACTOR_OF_QUADRARTIC", [Collect_geom2.FACTOR_OF_QUADRARTIC])) (fun fst_arg -> (use_arg_then2 ("a_neq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("disc_ge0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 207    ((((use_arg_then2 ("x_root", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Sphere.quadratic_root_plus", [Sphere.quadratic_root_plus]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_neq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))));
 208    ((repeat_tactic 1 9 (((use_arg_then2 ("REAL_SUB_0", [REAL_SUB_0]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN ((THENL) case [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); ALL_TAC]) THEN ((TRY done_tac)) THEN (move ["x_eq"]));
 209    ((fun arg_tac -> arg_tac (Arg_term (`x <= &0`))) (term_tac (have_gen_tac []ALL_TAC)));
 210    (((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] []))));
 211    ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`&0 <= u ==> (--b - u) / (&2 * a) <= &0`))) (term_tac (have_gen_tac ["u"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((((use_arg_then2 ("SQRT_POS_LE", [SQRT_POS_LE]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
 212    ((BETA_TAC THEN (move ["u_ge0"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (REAL_ARITH `!x. x <= &0 <=> ~(&0 < x)`)))(thm_tac (new_rewrite [] [])))));
 213    ((((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_POS_LT", [REAL_MUL_POS_LT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))));
 214    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`&0 < inv (&2 * a)`))) (term_tac (have_gen_tac [](move ["h1"])))) (((((use_arg_then2 ("REAL_LT_INV", [REAL_LT_INV]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LT_MUL", [REAL_LT_MUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("a_gt0", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)));
 215    ((((use_arg_then2 ("h1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("real_lt", [real_lt])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_LE_LT", [REAL_LE_LT]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("h1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
 216    ((((use_arg_then2 ("b_ge0", [])) (disch_tac [])) THEN (clear_assumption "b_ge0") THEN ((use_arg_then2 ("u_ge0", [])) (disch_tac [])) THEN (clear_assumption "u_ge0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 217    ((THENL_FIRST) ((((use_arg_then2 ("REAL_LE_LT", [REAL_LE_LT]))(thm_tac (new_rewrite [] [])))) THEN case) ((((use_arg_then2 ("x_ge0", [])) (disch_tac [])) THEN (clear_assumption "x_ge0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
 218    (BETA_TAC THEN (move ["x_eq0"]));
 219    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`c = &0`))) (term_tac (have_gen_tac [](move ["c_eq0"])))) ((((use_arg_then2 ("x_root", [])) (disch_tac [])) THEN (clear_assumption "x_root") THEN BETA_TAC) THEN ((((use_arg_then2 ("x_eq0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_RZERO", [REAL_MUL_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ADD_LID", [REAL_ADD_LID]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
 220    ((((use_arg_then2 ("Sphere.quadratic_root_plus", [Sphere.quadratic_root_plus]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("c_eq0", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_RZERO", [REAL_MUL_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_SUB_RZERO", [REAL_SUB_RZERO]))(thm_tac (new_rewrite [] [])))));
 221    (((((use_arg_then2 ("POW_2_SQRT", [POW_2_SQRT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("REAL_ADD_LINV", [REAL_ADD_LINV]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_LZERO", [REAL_MUL_LZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_eq0", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 222 ];;
 223
 224 (* Lemma quadratic_root_plus_gt_eq *)
 225 let quadratic_root_plus_gt_eq = Sections.section_proof ["a";"b";"c";"x";"y"]
 226 `&0 < a /\ &0 <= b pow 2 - &4 * a * c
 227         /\ a * x pow 2 + b * x + c = &0 /\ a * y pow 2 + b * y + c = &0 /\ y < x
 228         ==> quadratic_root_plus (a,b,c) = x`
 229 [
 230    (BETA_TAC THEN (case THEN (move ["a_gt0"])) THEN (case THEN (move ["disc_ge0"])) THEN (case THEN (move ["x_root"])) THEN (case THEN (move ["y_root"])) THEN (move ["y_lt_x"]));
 231    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(a = &0)`))) (term_tac (have_gen_tac [](move ["a_neq"])))) ((((use_arg_then2 ("a_gt0", [])) (disch_tac [])) THEN (clear_assumption "a_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
 232    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Collect_geom2.FACTOR_OF_QUADRARTIC", [Collect_geom2.FACTOR_OF_QUADRARTIC])) (fun fst_arg -> (use_arg_then2 ("a_neq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("disc_ge0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["h"])));
 233    ((((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("y", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("x_root", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("y_root", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_neq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))))));
 234    (((repeat_tactic 1 9 (((use_arg_then2 ("REAL_SUB_0", [REAL_SUB_0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Sphere.quadratic_root_plus", [Sphere.quadratic_root_plus]))(gsym_then (thm_tac (new_rewrite [1] [])))))) THEN ALL_TAC THEN ((THENL) case [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); ALL_TAC]) THEN ((TRY done_tac)) THEN (move ["x_eq"]));
 235    ((THENL_LAST) ((case THEN (move ["y_eq"])) THEN (((use_arg_then2 ("y_lt_x", [])) (disch_tac [])) THEN (clear_assumption "y_lt_x") THEN BETA_TAC) THEN ((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))))) ((arith_tac) THEN (done_tac)));
 236    ((THENL_FIRST) ((repeat_tactic 1 9 (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LT_RMUL_EQ", [REAL_LT_RMUL_EQ]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("REAL_LT_INV", [REAL_LT_INV]))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("REAL_LT_MUL", [REAL_LT_MUL]))(fun tmp_arg1 -> (use_arg_then2 ("a_gt0", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] [])))))) ((arith_tac) THEN (done_tac)));
 237    ((((fun arg_tac -> (use_arg_then2 ("SQRT_POS_LE", [SQRT_POS_LE])) (fun fst_arg -> (use_arg_then2 ("disc_ge0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 238 ];;
 239
 240 (* Lemma quadratic_root_plus_disc0_eq *)
 241 let quadratic_root_plus_disc0_eq = Sections.section_proof ["a";"b";"c";"x"]
 242 `~(a = &0) /\ b pow 2 - &4 * a * c = &0
 243         /\ a * x pow 2 + b * x + c = &0
 244         ==> quadratic_root_plus (a,b,c) = x`
 245 [
 246    (BETA_TAC THEN (case THEN (move ["a_neq0"])) THEN (case THEN (move ["disc0"])) THEN (move ["x_root"]));
 247    (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Collect_geom2.FACTOR_OF_QUADRARTIC", [Collect_geom2.FACTOR_OF_QUADRARTIC])) (fun fst_arg -> (use_arg_then2 ("a_neq0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("b", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("c", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN (ANTS_TAC));
 248    (((((use_arg_then2 ("disc0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_REFL", [REAL_LE_REFL]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 249    ((((use_arg_then2 ("x_root", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_neq0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))));
 250    (((repeat_tactic 1 9 (((use_arg_then2 ("REAL_SUB_0", [REAL_SUB_0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Sphere.quadratic_root_plus", [Sphere.quadratic_root_plus]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN ((THENL) case [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); ALL_TAC]) THEN ((TRY done_tac)));
 251    ((((((use_arg_then2 ("disc0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SQRT_0", [SQRT_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_SUB_RZERO", [REAL_SUB_RZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_RID", [REAL_ADD_RID]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 252 ];;
 253
 254 (* Finalization of the section Misc *)
 255 let delta_y_pos = Sections.finalize_theorem delta_y_pos;;
 256 let quadratic_root_plus_works = Sections.finalize_theorem quadratic_root_plus_works;;
 257 let quadratic_root_plus_eq = Sections.finalize_theorem quadratic_root_plus_eq;;
 258 let quadratic_root_plus_gt_eq = Sections.finalize_theorem quadratic_root_plus_gt_eq;;
 259 let quadratic_root_plus_disc0_eq = Sections.finalize_theorem quadratic_root_plus_disc0_eq;;
 260 Sections.end_section "Misc";;
 261
 262 (* Section FullySurrounded *)
 263 Sections.begin_section "FullySurrounded";;
 264 (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
 265 (Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));;
 266 (Sections.add_section_hyp "fanV" (`FAN (vec 0,V,E)`));;
 267 (Sections.add_section_hyp "f_surr" (`fully_surrounded (V,E)`));;
 268
 269 (* Let dart1_eq *)
 270 Sections.add_section_lemma "dart1_eq" (Sections.section_proof []
 271 `dart_of_fan (V,E) = dart1_of_fan (V,E)`
 272 [
 273    ((((use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 274 ]);;
 275
 276 (* Let confV *)
 277 Sections.add_section_lemma "confV" (Sections.section_proof []
 278 `conforming_fan (vec 0,V,E)`
 279 [
 280    ((((use_arg_then2 ("fully_surrounded_imp_conforming", [fully_surrounded_imp_conforming]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 281 ]);;
 282
 283 (* Let dartH *)
 284 Sections.add_section_lemma "dartH" (Sections.section_proof []
 285 `dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E)`
 286 [
 287    ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 288 ]);;
 289
 290 (* Lemma dart_leads_into_eq1 *)
 291 let dart_leads_into_eq1 = Sections.section_proof ["v";"w"]
 292 `v,w IN dart_of_fan (V,E)
 293         ==> dart_leads_into (vec 0) V E v w
 294                 = dartset_leads_into_fan (vec 0) V E
 295                         (IMAGE (ext_dart (V,E)) (face (hypermap_of_fan (V,E)) (v,w)))`
 296 [
 297    (BETA_TAC THEN (move ["vw_in"]));
 298    ((fun arg_tac -> (use_arg_then2 ("fan_hypermaps_iso_explicit2", [fan_hypermaps_iso_explicit2])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso"])));
 299    ((fun arg_tac -> arg_tac (Arg_term (`ext_dart _`))) (term_tac (set_tac "h")));
 300    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
 301    ((((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 302    ((fun arg_tac -> arg_tac (Arg_term (`face _1 _2`))) (term_tac (set_tac "f1")));
 303    ((THENL_ROT (-1)) (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Planarity.DARTSET_LEADS_INTO_FAN", [Planarity.DARTSET_LEADS_INTO_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`h (v,w)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
 304    (((((use_arg_then2 ("h_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ext_dart", [ext_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Fan.pr2", [Fan.pr2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Fan.pr3", [Fan.pr3]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 305    ((((use_arg_then2 ("fully_surrounded_imp_fan80", [fully_surrounded_imp_fan80]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] []))))));
 306    (((((use_arg_then2 ("face_refl", [face_refl]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (simp_tac) THEN (move ["u"]) THEN (move ["uV"]));
 307    ((((use_arg_then2 ("fully_surrounded_card_set_of_edge1", [fully_surrounded_card_set_of_edge1]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 308 ];;
 309
 310 (* Lemma dart_leads_into_same *)
 311 let dart_leads_into_same = Sections.section_proof ["f";"v";"w";"x";"y"]
 312 `f IN face_set (hypermap_of_fan (V,E))
 313         /\ (v,w) IN f /\ (x,y) IN f
 314         ==> dart_leads_into (vec 0) V E v w = dart_leads_into (vec 0) V E x y`
 315 [
 316    (BETA_TAC THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (case THEN (case THEN ((move ["a"]) THEN (move ["b"])))) THEN (case THEN (move ["ab_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (case THEN ((move ["vw_in"]) THEN (move ["xy_in"]))));
 317    ((fun arg_tac -> arg_tac (Arg_term (`x,y IN dart_of_fan (V,E) /\ v,w IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["all_in"]))));
 318    (((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (use_arg_then2 ("xy_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 319    ((repeat_tactic 1 9 (((use_arg_then2 ("dart_leads_into_eq1", [dart_leads_into_eq1]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 320    (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`a,b`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`a,b`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 321 ];;
 322
 323 (* Lemma fully_surrounded_sol *)
 324 let fully_surrounded_sol = Sections.section_proof ["v";"w"]
 325 `v,w IN dart_of_fan (V,E)
 326    ==> sol (vec 0) (dart_leads_into (vec 0) V E v w)
 327         = &2 * pi + sum (face (hypermap_of_fan (V,E)) (v,w)) (\x. azim_dart (V,E) x - pi)`
 328 [
 329    (BETA_TAC THEN (move ["vw_in"]));
 330    ((fun arg_tac -> (use_arg_then2 ("fan_hypermaps_iso_explicit2", [fan_hypermaps_iso_explicit2])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso"])));
 331    ((((use_arg_then2 ("confV", [])) (disch_tac [])) THEN (clear_assumption "confV") THEN BETA_TAC) THEN ((((use_arg_then2 ("Conforming.conforming_fan", [Conforming.conforming_fan]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE Conforming.conforming_solid_angle_fan)))(thm_tac (new_rewrite [] []))))));
 332    (BETA_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (case THEN (move ["f_sol"])) THEN (move ["_"]));
 333    ((((use_arg_then2 ("dart_leads_into_eq1", [dart_leads_into_eq1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_sol", []))(thm_tac (new_rewrite [] [])))));
 334    (((((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 335    ((congr_tac (`_1 + _2:real`)) THEN ((TRY done_tac)));
 336    ((fun arg_tac -> arg_tac (Arg_term (`x IN face (hypermap_of_fan (V,E)) (v,w) ==> x IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac ["x"](move ["in_face"]))));
 337    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 338    (((use_arg_then2 ("SUM_IMAGE", [SUM_IMAGE]))(thm_tac (new_rewrite [] []))));
 339    (BETA_TAC THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("in_face", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (move ["x_in"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("in_face", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (move ["y_in"]) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))));
 340    (((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 341    (((use_arg_then2 ("SUM_EQ", [SUM_EQ])) (thm_tac apply_tac)) THEN (BETA_TAC THEN (case THEN ((move ["a"]) THEN (move ["b"]))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("in_face", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["d_in"])));
 342    (((((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("ext_dart", [ext_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Fan.pr2", [Fan.pr2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Fan.pr3", [Fan.pr3]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("azim_dart_eq_azim_fan", [azim_dart_eq_azim_fan]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 343 ];;
 344
 345 (* Lemma fully_surrounded_sum_sol *)
 346 let fully_surrounded_sum_sol = Sections.section_proof []
 347 `sum (face_set (hypermap_of_fan (V,E)))
 348         (\f. sol (vec 0) (dartset_leads_into_fan (vec 0) V E  (IMAGE (ext_dart (V,E)) f)))
 349         = &4 * pi`
 350 [
 351    ((fun arg_tac -> (use_arg_then2 ("fan_hypermaps_iso_explicit2", [fan_hypermaps_iso_explicit2])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso"])));
 352    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Conforming.SUM_SOL_IN_FACE_SET_EQ_4PI", [Conforming.SUM_SOL_IN_FACE_SET_EQ_4PI])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("confV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 353    ((THENL_ROT (-1)) ((((fun arg_tac -> (use_arg_then2 ("iso_face_set", [iso_face_set])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUM_IMAGE", [SUM_IMAGE]))(thm_tac (new_rewrite [] []))))));
 354    ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("SUM_EQ", [SUM_EQ])) (thm_tac apply_tac)) THEN (move ["f"]) THEN (move ["_"]) THEN (simp_tac)) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 355    (BETA_TAC THEN (move ["f1"]) THEN (move ["f2"]));
 356    (BETA_TAC THEN (case THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["x"])) THEN (case THEN (move ["x_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (case THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
 357    ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("image_inj_gen", [image_inj_gen])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart (hypermap_of_fan (V,E))`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 358    ((repeat_tactic 1 9 (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
 359    (((fun arg_tac -> (use_arg_then2 ("hyp_iso_inj", [hyp_iso_inj])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
 360 ];;
 361
 362 (* Lemma fully_surrounded_not_coplanar *)
 363 let fully_surrounded_not_coplanar = Sections.section_proof ["v";"w"]
 364 `v,w IN dart_of_fan (V,E)
 365         ==> ~(coplanar {vec 0, v, w, sigma_fan (vec 0) V E v w})`
 366 [
 367    ((BETA_TAC THEN (move ["vw_in"])) THEN (((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in1"])));
 368    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sigma_in_dart1", [sigma_in_dart1])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["vw'_in"])));
 369    ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _1 V _2 v w`))) (term_tac (set_tac "w'")));
 370    ((fun arg_tac -> arg_tac (Arg_term (`{vec 0, v, w, w'} = {vec 0, w', v, w}`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
 371    ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem ((GEN_ALL o CONJUNCT2 o CONJUNCT2) Collect_geom.PER_SET3))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 372    ((((fun arg_tac -> (use_arg_then2 ("Planarity.properties_fully_surrounded", [Planarity.properties_fully_surrounded])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 373    ((((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_azim_dart_eq_azim", [fully_surrounded_azim_dart_eq_azim])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))));
 374    ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1])) (fun fst_arg -> (use_arg_then2 ("V", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("vw_in1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_switch", [dart1_switch]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw'_in", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("AZIM_DART_POS", [AZIM_DART_POS])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
 375    ((((use_arg_then2 ("f_surr", [])) (disch_tac [])) THEN (clear_assumption "f_surr") THEN BETA_TAC) THEN ((((use_arg_then2 ("fully_surrounded", [fully_surrounded]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 376 ];;
 377
 378 (* Lemma fully_surrounded_delta_pos *)
 379 let fully_surrounded_delta_pos = Sections.section_proof ["v";"w"]
 380 `v,w IN dart_of_fan (V,E) ==>
 381                 let w' = sigma_fan (vec 0) V E v w in
 382                 let y1 = norm v in
 383                 let y2 = norm w in
 384                 let y3 = norm w' in
 385                 let y4 = dist (w,w') in
 386                 let y5 = dist (v,w') in
 387                 let y6 = dist (v,w) in
 388                         &0 < delta_y y1 y2 y3 y4 y5 y6`
 389 [
 390    (((((use_arg_then2 ("Sphere.delta_y", [Sphere.delta_y]))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in"])) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))));
 391    ((((use_arg_then2 ("DELTA_EQ_DELTA_X", [DELTA_EQ_DELTA_X]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Trigonometry1.DIST_L_ZERO", [Trigonometry1.DIST_L_ZERO]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] [])))))));
 392    (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom2.POS_EQ_NOT_COPLANANR)))(thm_tac (new_rewrite [] []))));
 393    ((THENL_FIRST) ((((use_arg_then2 ("Ckqowsa_3_points.coplanar_eq_coplanar_alt", [Ckqowsa_3_points.coplanar_eq_coplanar_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("DIMINDEX_3", [DIMINDEX_3]))(thm_tac (new_rewrite [] [])))))) ((arith_tac) THEN (done_tac)));
 394    (((use_arg_then2 ("fully_surrounded_not_coplanar", [fully_surrounded_not_coplanar])) (disch_tac [])) THEN (clear_assumption "fully_surrounded_not_coplanar") THEN (exact_tac));
 395 ];;
 396
 397 (* Lemma fully_surrounded_azim_eq_dih_y *)
 398 let fully_surrounded_azim_eq_dih_y = Sections.section_proof ["v";"w"]
 399 `v,w IN dart_of_fan (V,E) ==>
 400          let w' = sigma_fan (vec 0) V E v w in
 401          let y1 = norm v in
 402          let y2 = norm w in
 403          let y3 = norm w' in
 404          let y4 = dist (w,w') in
 405          let y5 = dist (v,w') in
 406          let y6 = dist (v,w) in
 407                 azim_dart (V,E) (v,w) = dih_y y1 y2 y3 y4 y5 y6`
 408 [
 409    ((BETA_TAC THEN (move ["vw_in"])) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))) THEN (((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in1"])));
 410    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sigma_in_dart1", [sigma_in_dart1])) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["vw'_in"])));
 411    ((((use_arg_then2 ("fully_surrounded_azim_dart_eq_azim", [fully_surrounded_azim_dart_eq_azim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("AZIM_DIVH", [AZIM_DIVH]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("DART1_NOT_COLLINEAR", [DART1_NOT_COLLINEAR])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 412    ((((use_arg_then2 ("fully_surrounded_azim_dart_eq_azim", [fully_surrounded_azim_dart_eq_azim]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 413    ((((use_arg_then2 ("f_surr", [])) (disch_tac [])) THEN (clear_assumption "f_surr") THEN BETA_TAC) THEN ((((use_arg_then2 ("fully_surrounded", [fully_surrounded]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))));
 414    ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE DIHV_EQ_DIH_Y)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("DART1_NOT_COLLINEAR", [DART1_NOT_COLLINEAR])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 415    ((repeat_tactic 1 9 (((use_arg_then2 ("Trigonometry1.DIST_L_ZERO", [Trigonometry1.DIST_L_ZERO]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 416 ];;
 417
 418 (* Lemma fully_surrounded_sol_eq_sol_y *)
 419 let fully_surrounded_sol_eq_sol_y = Sections.section_proof ["v";"w"]
 420 `v,w IN dart_of_fan (V,E) /\
 421         CARD (face (hypermap_of_fan (V,E)) (v,w)) = 3 ==>
 422                  let w' = sigma_fan (vec 0) V E v w in
 423                  let y1 = norm v in
 424                  let y2 = norm w in
 425                  let y3 = norm w' in
 426                  let y4 = dist (w,w') in
 427                  let y5 = dist (v,w') in
 428                  let y6 = dist (v,w) in
 429         sol (vec 0) (dart_leads_into (vec 0) V E v w) = sol_y y1 y2 y3 y4 y5 y6`
 430 [
 431    ((BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card3"])))) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))) THEN (((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in1"])));
 432    ((((use_arg_then2 ("fully_surrounded_sol", [fully_surrounded_sol]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 433    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE TRIANGULAR_FACE))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["f_eq"]) THEN (move ["eqs"])))));
 434    ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
 435    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
 436    ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart_of_fan (V,E) /\ w,w' IN dart_of_fan (V,E) /\ w',v IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["all_in"]))));
 437    ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 ((split_tac))) THEN ((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`face H (v,w)`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_INSERT", [IN_INSERT]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 438    ((fun arg_tac -> arg_tac (Arg_term (`~(v = w) /\ ~(w' = v) /\ ~(w = w')`))) (term_tac (have_gen_tac [](move ["neqs"]))));
 439    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ", [PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dart1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
 440    ((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("SUM_SING", [SUM_SING]))(fun tmp_arg1 -> (use_arg_then2 ("SUM_CLAUSES", [SUM_CLAUSES]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("FINITE_INSERT", [FINITE_INSERT]))(fun tmp_arg1 -> (use_arg_then2 ("FINITE_EMPTY", [FINITE_EMPTY]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 441    ((repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("IN_SING", [IN_SING]))(fun tmp_arg1 -> (use_arg_then2 ("IN_INSERT", [IN_INSERT]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("neqs", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("neqs", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac));
 442    ((repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE fully_surrounded_azim_eq_dih_y)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))));
 443    (((((use_arg_then2 ("Sphere.sol_y", [Sphere.sol_y]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac));
 444 ];;
 445
 446 (* Lemma tauVEF_alt1 *)
 447 let tauVEF_alt1 = Sections.section_proof ["v";"w"]
 448 `v,w IN dart_of_fan (V,E)
 449         ==> let f = face (hypermap_of_fan (V,E)) (v,w) in
 450                 tauVEF (V,E,f) = sol (vec 0) (dart_leads_into (vec 0) V E v w)
 451                   + (&2 - &(CARD f)) * sol0
 452                   - sol0 / pi * sum f (\x. azim_dart (V,E) x * (lmfun (h_dart x) - &1))`
 453 [
 454    ((BETA_TAC THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
 455    ((((use_arg_then2 ("Tame_defs.tauVEF", [Tame_defs.tauVEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fully_surrounded_sol", [fully_surrounded_sol]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 456    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
 457    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_FINITE", [FACE_FINITE])) (fun fst_arg -> (use_arg_then2 ("H", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["fin_f"])));
 458    (((fun arg_tac -> arg_tac (Arg_theorem (REAL_ARITH `!a b c. a * (&1 + b * (&1 - c)) = a - b * (a * (c - &1))`)))(thm_tac (new_rewrite [] []))));
 459    (((repeat_tactic 1 9 (((use_arg_then2 ("SUM_SUB", [SUM_SUB]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("SUM_LMUL", [SUM_LMUL]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("SUM_CONST", [SUM_CONST])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`pi`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (arith_tac) THEN (done_tac));
 460 ];;
 461
 462 (* Lemma tauVEF_alt2 *)
 463 let tauVEF_alt2 = Sections.section_proof ["v";"w"]
 464 `v,w IN dart_of_fan (V,E)
 465         ==> let f = face (hypermap_of_fan (V,E)) (v,w) in
 466           tauVEF (V,E,f) = sol (vec 0) (dart_leads_into (vec 0) V E v w) * (&1 + sol0 / pi)
 467                         - sol0 / pi * sum f (\x. azim_dart (V,E) x * lmfun (h_dart x))`
 468 [
 469    ((BETA_TAC THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
 470    ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE tauVEF_alt1)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("fully_surrounded_sol", [fully_surrounded_sol]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 471    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
 472    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_FINITE", [FACE_FINITE])) (fun fst_arg -> (use_arg_then2 ("H", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["fin_f"])));
 473    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a * (b - &1) = a * b - a`))) (term_tac (have_gen_tac ["a"; "b"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
 474    ((repeat_tactic 1 9 (((use_arg_then2 ("SUM_SUB", [SUM_SUB]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("SUM_CONST", [SUM_CONST])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`pi`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 475    ((((use_arg_then2 ("PI_POS", [PI_POS])) (disch_tac [])) THEN (clear_assumption "PI_POS") THEN BETA_TAC) THEN (CONV_TAC REAL_FIELD) THEN (done_tac));
 476 ];;
 477
 478 (* Lemma tauVEF_alt2_alt *)
 479 let tauVEF_alt2_alt = Sections.section_proof ["f"]
 480 `f IN face_set (hypermap_of_fan (V,E))
 481    ==> tauVEF (V,E,f)
 482         = sol (vec 0) (dartset_leads_into_fan (vec 0) V E  (IMAGE (ext_dart (V,E)) f))
 483                 * (&1 + sol0 / pi)
 484                 - sol0 / pi * sum f (\x. azim_dart (V,E) x * lmfun (h_dart x))`
 485 [
 486    (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (case THEN ((move ["v"]) THEN (move ["w"]))))) THEN ((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["vw_in"])) THEN (move ["f_eq"])));
 487    (((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE tauVEF_alt2)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_leads_into_eq1", [dart_leads_into_eq1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 488 ];;
 489
 490 (* Lemma tauVEF_alt3 *)
 491 let tauVEF_alt3 = Sections.section_proof ["v";"w"]
 492 `v,w IN dart_of_fan (V,E)
 493         ==> let f = face (hypermap_of_fan (V,E)) (v,w) in
 494         tauVEF (V,E,f) = sum f (\x. (&1 + sol0 / pi * (&1 - lmfun (h_dart x)))
 495         * azim_dart (V,E) x - pi - sol0) + &2 * (pi + sol0)`
 496 [
 497    ((BETA_TAC THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
 498    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a * x - b - c = x * a - (b + c):real`))) (term_tac (have_gen_tac ["a"; "x"; "b"; "c"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
 499    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
 500    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_FINITE", [FACE_FINITE])) (fun fst_arg -> (use_arg_then2 ("H", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["fin_f"])));
 501    ((((use_arg_then2 ("SUM_SUB", [SUM_SUB]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("SUM_CONST", [SUM_CONST])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`pi + sol0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 502    ((((use_arg_then2 ("Tame_defs.tauVEF", [Tame_defs.tauVEF]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 503 ];;
 504
 505 (* Lemma sum_tauVEF_upper_bound *)
 506 let sum_tauVEF_upper_bound = Sections.section_proof []
 507 `&12 <= scriptL V ==>
 508          sum (face_set (hypermap_of_fan (V,E))) (\f. tauVEF (V,E,f))
 509                 <= &4 * pi - &20 * sol0`
 510 [
 511    ((((fun arg_tac -> (use_arg_then2 ("SUM_EQ", [SUM_EQ])) (fun fst_arg -> (use_arg_then2 ("tauVEF_alt2_alt", [tauVEF_alt2_alt])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (move ["ineq"]));
 512    ((((use_arg_then2 ("SUM_SUB", [SUM_SUB]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("SUM_LMUL", [SUM_LMUL])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`sol0 / pi`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("SUM_RMUL", [SUM_RMUL])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&1 + sol0 / pi`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
 513    (((use_arg_then2 ("fully_surrounded_sum_sol", [fully_surrounded_sum_sol]))(thm_tac (new_rewrite [] []))));
 514    ((((use_arg_then2 ("Tame_defs.face_set_of_fan", [Tame_defs.face_set_of_fan]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Hrxefdm_tame.HRXEFDM_lemma1", [Hrxefdm_tame.HRXEFDM_lemma1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 515    ((fun arg_tac -> arg_tac (Arg_term (`(&4 * pi) * (&1 + s / pi) - s / pi * &2 * pi * v = &4 * pi - (&2 * v - &4) * s`))) (term_tac (have_gen_tac ["v"; "s"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
 516    ((((use_arg_then2 ("PI_NZ", [PI_NZ])) (disch_tac [])) THEN (clear_assumption "PI_NZ") THEN BETA_TAC) THEN (CONV_TAC REAL_FIELD) THEN (done_tac));
 517    ((repeat_tactic 1 9 (((use_arg_then2 ("real_sub", [real_sub]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_LADD", [REAL_LE_LADD]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_RMUL", [REAL_LE_RMUL]))(thm_tac (new_rewrite [] [])))));
 518    (((fun arg_tac -> (use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE])) (fun fst_arg -> (use_arg_then2 ("sol0_POS", [sol0_POS])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))));
 519    ((((use_arg_then2 ("ineq", [])) (disch_tac [])) THEN (clear_assumption "ineq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 520 ];;
 521
 522 (* Lemma fully_surrounded_dot_cross *)
 523 let fully_surrounded_dot_cross = Sections.section_proof ["v";"w"]
 524 `v,w IN dart_of_fan (V,E)
 525         ==> &0 < v dot (w cross sigma_fan (vec 0) V E v w)`
 526 [
 527    (BETA_TAC THEN (move ["vw_in"]));
 528    ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
 529    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Trigonometry.JBDNJJB", [Trigonometry.JBDNJJB])) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 530    ((((use_arg_then2 ("Trigonometry2.re_eqvl", [Trigonometry2.re_eqvl]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["t"])) THEN (case THEN (move ["t_gt0"])));
 531    (((((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("fully_surrounded_azim_dart_eq_azim", [fully_surrounded_azim_dart_eq_azim]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["sin_eq"]));
 532    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`&0 < sin (azim_dart (V,E) (v,w))`))) (term_tac (have_gen_tac []ALL_TAC))));
 533    ((((use_arg_then2 ("sin_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Trigonometry1.cross_triple", [Trigonometry1.cross_triple]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_SYM", [DOT_SYM]))(thm_tac (new_rewrite [] [])))));
 534    ((((use_arg_then2 ("REAL_MUL_POS_LT", [REAL_MUL_POS_LT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("t_gt0", [])) (disch_tac [])) THEN (clear_assumption "t_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 535    ((((use_arg_then2 ("SIN_POS_PI", [SIN_POS_PI]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("AZIM_DART_POS", [AZIM_DART_POS]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 536    ((((use_arg_then2 ("f_surr", [])) (disch_tac [])) THEN (clear_assumption "f_surr") THEN BETA_TAC) THEN ((((use_arg_then2 ("fully_surrounded", [fully_surrounded]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 537 ];;
 538
 539 (* Section BallAnnulus *)
 540 Sections.begin_section "BallAnnulus";;
 541 (Sections.add_section_hyp "subV" (`V SUBSET ball_annulus`));;
 542
 543 (* Let v_norm *)
 544 Sections.add_section_lemma "v_norm" (Sections.section_proof ["v"]
 545 `v IN V ==> norm v <= &2 * h0 /\ &2 <= norm v`
 546 [
 547    ((in_tac ["subV"] false (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("subV", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN ((((use_arg_then2 ("Ckqowsa_3_points.in_ball_annulus", [Ckqowsa_3_points.in_ball_annulus]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
 548 ]);;
 549
 550 (* Lemma fully_surrounded_lnazim *)
 551 let fully_surrounded_lnazim = Sections.section_proof ["v";"w"]
 552 `v,w IN dart_of_fan (V,E) ==>
 553          let w' = sigma_fan (vec 0) V E v w in
 554          let y1 = norm v in
 555          let y2 = norm w in
 556          let y3 = norm w' in
 557          let y4 = dist (w,w') in
 558          let y5 = dist (v,w') in
 559          let y6 = dist (v,w) in
 560                 azim_dart (V,E) (v,w) * lmfun (h_dart (v,w)) = lnazim y1 y2 y3 y4 y5 y6`
 561 [
 562    ((BETA_TAC THEN (move ["vw_in"])) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))));
 563    ((((use_arg_then2 ("Sphere.lnazim", [Sphere.lnazim]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE fully_surrounded_azim_eq_dih_y))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))));
 564    (((((use_arg_then2 ("REAL_MUL_SYM", [REAL_MUL_SYM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ly_EQ_lmfun", [ly_EQ_lmfun]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("v_norm", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 565 ];;
 566
 567 (* Lemma fully_surrounded_tau_eq_taum *)
 568 let fully_surrounded_tau_eq_taum = Sections.section_proof ["v";"w"]
 569 `v,w IN dart_of_fan (V,E)
 570         /\ CARD (face (hypermap_of_fan (V,E)) (v,w)) = 3
 571         ==>     let w' = sigma_fan (vec 0) V E v w in
 572                 let y1 = norm v in
 573                 let y2 = norm w in
 574                 let y3 = norm w' in
 575                 let y4 = dist (w,w') in
 576                 let y5 = dist (v,w') in
 577                 let y6 = dist (v,w) in
 578                 tauVEF (V,E,face (hypermap_of_fan (V,E)) (v,w)) = taum y1 y2 y3 y4 y5 y6`
 579 [
 580    ((BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card3"])))) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))) THEN (((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in1"])));
 581    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE TRIANGULAR_FACE))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["f_eq"]) THEN (move ["eqs"])))));
 582    ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["dartH"]) THEN (move ["_"])))));
 583    ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
 584    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
 585    ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart_of_fan (V,E) /\ w,w' IN dart_of_fan (V,E) /\ w',v IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["all_in"]))));
 586    ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 ((split_tac))) THEN ((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`face H (v,w)`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_INSERT", [IN_INSERT]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 587    ((fun arg_tac -> arg_tac (Arg_term (`~(v = w) /\ ~(w' = v) /\ ~(w = w')`))) (term_tac (have_gen_tac [](move ["neqs"]))));
 588    (((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ", [PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dart1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
 589    ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE tauVEF_alt2)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))));
 590    ((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("SUM_SING", [SUM_SING]))(fun tmp_arg1 -> (use_arg_then2 ("SUM_CLAUSES", [SUM_CLAUSES]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("FINITE_INSERT", [FINITE_INSERT]))(fun tmp_arg1 -> (use_arg_then2 ("FINITE_EMPTY", [FINITE_EMPTY]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 591    ((repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("IN_SING", [IN_SING]))(fun tmp_arg1 -> (use_arg_then2 ("IN_INSERT", [IN_INSERT]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("neqs", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("neqs", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac));
 592    ((repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE fully_surrounded_lnazim)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))));
 593    ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE fully_surrounded_sol_eq_sol_y)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))));
 594    (((((use_arg_then2 ("Sphere.taum", [Sphere.taum]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("sol0_over_pi_EQ_const1", [sol0_over_pi_EQ_const1]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 595 ];;
 596
 597 (* Finalization of the section BallAnnulus *)
 598 let fully_surrounded_lnazim = Sections.finalize_theorem fully_surrounded_lnazim;;
 599 let fully_surrounded_tau_eq_taum = Sections.finalize_theorem fully_surrounded_tau_eq_taum;;
 600 Sections.end_section "BallAnnulus";;
 601
 602 (* Finalization of the section FullySurrounded *)
 603 let dart_leads_into_eq1 = Sections.finalize_theorem dart_leads_into_eq1;;
 604 let dart_leads_into_same = Sections.finalize_theorem dart_leads_into_same;;
 605 let fully_surrounded_sol = Sections.finalize_theorem fully_surrounded_sol;;
 606 let fully_surrounded_sum_sol = Sections.finalize_theorem fully_surrounded_sum_sol;;
 607 let fully_surrounded_not_coplanar = Sections.finalize_theorem fully_surrounded_not_coplanar;;
 608 let fully_surrounded_delta_pos = Sections.finalize_theorem fully_surrounded_delta_pos;;
 609 let fully_surrounded_azim_eq_dih_y = Sections.finalize_theorem fully_surrounded_azim_eq_dih_y;;
 610 let fully_surrounded_sol_eq_sol_y = Sections.finalize_theorem fully_surrounded_sol_eq_sol_y;;
 611 let tauVEF_alt1 = Sections.finalize_theorem tauVEF_alt1;;
 612 let tauVEF_alt2 = Sections.finalize_theorem tauVEF_alt2;;
 613 let tauVEF_alt2_alt = Sections.finalize_theorem tauVEF_alt2_alt;;
 614 let tauVEF_alt3 = Sections.finalize_theorem tauVEF_alt3;;
 615 let sum_tauVEF_upper_bound = Sections.finalize_theorem sum_tauVEF_upper_bound;;
 616 let fully_surrounded_dot_cross = Sections.finalize_theorem fully_surrounded_dot_cross;;
 617 let fully_surrounded_lnazim = Sections.finalize_theorem fully_surrounded_lnazim;;
 618 let fully_surrounded_tau_eq_taum = Sections.finalize_theorem fully_surrounded_tau_eq_taum;;
 619 Sections.end_section "FullySurrounded";;
 620
 621 (* Section EnclosedTauq *)
 622 Sections.begin_section "EnclosedTauq";;
 623
 624 (* Lemma taum_sym *)
 625 let taum_sym = Sections.section_proof ["y1";"y2";"y3";"y4";"y5";"y6"]
 626 `taum y1 y2 y3 y4 y5 y6 = taum y3 y2 y1 y6 y5 y4`
 627 [
 628    ((use_arg_then2 ("Nonlinear_lemma.dih_y_sym", [Nonlinear_lemma.dih_y_sym])) (fun arg -> thm_tac MP_TAC arg THEN (move ["sym"])));
 629    ((((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Sphere.taum", [Sphere.taum]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Sphere.sol_y", [Sphere.sol_y]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Sphere.lnazim", [Sphere.lnazim]))(thm_tac (new_rewrite [] []))))));
 630    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sym", [])) (fun fst_arg -> (use_arg_then2 ("y3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("y2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sym", [])) (fun fst_arg -> (use_arg_then2 ("y2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("y1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sym", [])) (fun fst_arg -> (use_arg_then2 ("y1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("y3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
 631    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a + b + c - d = c + b + a - d:real`))) (term_tac (have_gen_tac ["a"; "b"; "c"; "d"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
 632    (((use_arg_then2 ("Sphere.sol_y", [Sphere.sol_y]))(gsym_then (thm_tac (new_rewrite [] [])))));
 633    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a + b + c = c + b + a:real`))) (term_tac (have_gen_tac ["a"; "b"; "c"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
 634    (((repeat_tactic 1 9 (((use_arg_then2 ("Sphere.lnazim", [Sphere.lnazim]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("Sphere.taum", [Sphere.taum]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 635 ];;
 636 (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
 637 (Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));;
 638 (Sections.add_section_hyp "fanV" (`FAN (vec 0,V,E)`));;
 639 (Sections.add_section_hyp "f_surr" (`fully_surrounded (V,E)`));;
 640
 641 (* Let dart1_eq *)
 642 Sections.add_section_lemma "dart1_eq" (Sections.section_proof []
 643 `dart_of_fan (V,E) = dart1_of_fan (V,E)`
 644 [
 645    ((((use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 646 ]);;
 647
 648 (* Let dartH *)
 649 Sections.add_section_lemma "dartH" (Sections.section_proof []
 650 `dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E)`
 651 [
 652    ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 653 ]);;
 654
 655 (* Lemma fully_surrounded_enclosed *)
 656 let fully_surrounded_enclosed = Sections.section_proof ["v";"w"]
 657 `v,w IN dart_of_fan (V,E)
 658         ==>     let w' = sigma_fan (vec 0) V E v w in
 659                 let u = sigma_fan (vec 0) V E w' v in
 660                 let y1 = norm v in
 661                 let y2 = norm w in
 662                 let y3 = norm w' in
 663                 let y4 = dist(w,w') in
 664                 let y5 = dist(v,w') in
 665                 let y6 = dist(v,w) in
 666                 let y7 = norm u in
 667                 let y8 = dist(w',u) in
 668                 let y9 = dist(w,u) in
 669         dist (v,u) = enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9`
 670 [
 671    ((BETA_TAC THEN (move ["vw_in"])) THEN (repeat_tactic 11 0 ((CONV_TAC let_CONV))));
 672    ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
 673    ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E w' v`))) (term_tac (set_tac "u")));
 674    (((use_arg_then2 ("Enclosed.enclosed", [Enclosed.enclosed]))(thm_tac (new_rewrite [] []))));
 675    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE Collect_geom2.CAYLEYR_5POINTS))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0:real^3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("u", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 676    ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DIST_0", [DIST_0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Mur.muR", [Mur.muR]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))));
 677    ((fun arg_tac -> arg_tac (Arg_term (`muR _1 _2 _3 _4 _5 _6 _7 _8 _9`))) (term_tac (set_tac "p")));
 678    (BETA_TAC THEN (move ["p0"]));
 679    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`quadratic_root_plus (abc_of_quadratic p) = dist (u,v) pow 2`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
 680    (((((use_arg_then2 ("POW_2_SQRT", [POW_2_SQRT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("DIST_POS_LE", [DIST_POS_LE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 681    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`?a b c x. (p = \x. a * x pow 2 + b * x + c)
 682         /\ &0 < a /\ &0 <= b pow 2 - &4 * a * c
 683         /\ (p (dist (x, v) * dist (x, v)) = &0 /\ dist (x, v) < dist (u, v)
 684                 \/ b pow 2 - &4 * a * c = &0)`))) (term_tac (have_gen_tac []ALL_TAC))));
 685    (BETA_TAC THEN (case THEN (move ["a"])) THEN (case THEN (move ["b"])) THEN (case THEN (move ["c"])) THEN (case THEN (move ["x"])) THEN (case THEN (move ["p_eq"])) THEN (case THEN (move ["a_gt0"])) THEN (case THEN (move ["disc_ge0"])) THEN (move ["h"]));
 686    ((((use_arg_then2 ("p_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Nonlinear_lemma.abc_quadratic", [Nonlinear_lemma.abc_quadratic]))(thm_tac (new_rewrite [] [])))));
 687    ((THENL_ROT (-1)) ((THENL) (((use_arg_then2 ("h", [])) (disch_tac [])) THEN (clear_assumption "h") THEN case) [((case THEN (move ["px0"])) THEN (move ["dist_lt"])); (move ["disc0"])]));
 688    (((use_arg_then2 ("quadratic_root_plus_disc0_eq", [quadratic_root_plus_disc0_eq])) (disch_tac [])) THEN (clear_assumption "quadratic_root_plus_disc0_eq") THEN (DISCH_THEN apply_tac));
 689    (((((use_arg_then2 ("disc0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_POS_NZ", [REAL_POS_NZ]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("p0", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("p_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 690    ((((use_arg_then2 ("quadratic_root_plus_gt_eq", [quadratic_root_plus_gt_eq])) (disch_tac [])) THEN (clear_assumption "quadratic_root_plus_gt_eq") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`dist (x, v) * dist (x, v)`))) (term_tac exists_tac)));
 691    ((((use_arg_then2 ("a_gt0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("disc_ge0", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] []))))));
 692    ((((use_arg_then2 ("px0", [])) (disch_tac [])) THEN (clear_assumption "px0") THEN ((use_arg_then2 ("p0", [])) (disch_tac [])) THEN (clear_assumption "p0") THEN BETA_TAC) THEN (((((use_arg_then2 ("p_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
 693    (((((use_arg_then2 ("REAL_LT_SQUARE_ABS", [REAL_LT_SQUARE_ABS]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("dist", [dist]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ABS_NORM", [REAL_ABS_NORM]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("dist", [dist]))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
 694    ((((use_arg_then2 ("p_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Mur.muRa)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom.LEMMA50)))(thm_tac (new_rewrite [] [])))));
 695    ((fun arg_tac -> arg_tac (Arg_term (`ups_x _1 _2 _3`))) (term_tac (set_tac "a")));
 696    ((fun arg_tac -> arg_tac (Arg_term (`cayleytr _1 _2 _3 _4 _5 _6 _7 _8 _9 _10`))) (term_tac (set_tac "b")));
 697    ((fun arg_tac -> arg_tac (Arg_term (`cayleyR _1 _2 _3 _4 _5 _6 _7 _8 _9 _10`))) (term_tac (set_tac "c")));
 698    ((fun arg_tac -> arg_tac (Arg_term (`reflection (w cross w') u`))) (term_tac (set_tac "y")));
 699    (((((use_arg_then2 ("a", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("b", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("c", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("y", [])) (term_tac exists_tac))) THEN (simp_tac)) THEN (split_tac));
 700    (((use_arg_then2 ("a_def", []))(gsym_then (thm_tac (new_rewrite [] [])))));
 701    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem ((GEN_ALL o let_RULE) Trigonometry2.NOT_COLLINEAR_IMP_UPS_LT))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0:real^3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 702    (((repeat_tactic 1 9 (((use_arg_then2 ("DIST_0", [DIST_0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN apply_tac));
 703    (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_not_coplanar", [fully_surrounded_not_coplanar])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("Planarity.notcoplanar_imp_notcollinear_fan", [Planarity.notcoplanar_imp_notcollinear_fan])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC);
 704    ((((((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom.PER_SET3)))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 705    (split_tac);
 706    ((((use_arg_then2 ("b_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("c_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom.DISCRIMINANT_OF_CAY)))(thm_tac (new_rewrite [] [])))));
 707    ((repeat_tactic 1 9 (((use_arg_then2 ("DELTA_EQ_DELTA_X", [DELTA_EQ_DELTA_X]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Sphere.delta_y", [Sphere.delta_y]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("u", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))));
 708    ((THENL_LAST) (repeat_tactic 1 9 (((use_arg_then2 ("REAL_LE_MUL", [REAL_LE_MUL]))(thm_tac (new_rewrite [] []))))) ((arith_tac) THEN (done_tac)));
 709    ((repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE delta_y_pos)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 710    (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_card_face_alt", [fully_surrounded_card_face_alt])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (move ["card_f"]));
 711    ((DISJ2_TAC) THEN ((((use_arg_then2 ("b_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("c_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom.DISCRIMINANT_OF_CAY)))(thm_tac (new_rewrite [] []))))));
 712    ((repeat_tactic 1 9 (((use_arg_then2 ("DELTA_EQ_DELTA_X", [DELTA_EQ_DELTA_X]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Sphere.delta_y", [Sphere.delta_y]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("u", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))));
 713    ((fun arg_tac -> arg_tac (Arg_term (`u = w`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
 714    (((((use_arg_then2 ("u_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE TRIANGULAR_FACE))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart1_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 715    ((repeat_tactic 1 9 (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (DISJ2_TAC) THEN (DISJ2_TAC));
 716    ((((use_arg_then2 ("Sphere.delta_y", [Sphere.delta_y]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DELTA_EQ_DELTA_X", [DELTA_EQ_DELTA_X]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Trigonometry1.DIST_L_ZERO", [Trigonometry1.DIST_L_ZERO]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] [])))))));
 717    ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE Collect_geom.POLFLZY)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Ckqowsa_3_points.coplanar_eq_coplanar_alt", [Ckqowsa_3_points.coplanar_eq_coplanar_alt]))(gsym_then (thm_tac (new_rewrite [] []))))));
 718    ((((use_arg_then2 ("DIMINDEX_3", [DIMINDEX_3]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 719    (((fun arg_tac -> arg_tac (Arg_theorem ((GEN_ALL o CONJUNCT2) Collect_geom2.PER_SET4)))(thm_tac (new_rewrite [] []))));
 720    ((((use_arg_then2 ("COPLANAR_SMALL", [COPLANAR_SMALL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_CLAUSES", [CARD_CLAUSES]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("FINITE_INSERT", [FINITE_INSERT]))(fun tmp_arg1 -> (use_arg_then2 ("FINITE_EMPTY", [FINITE_EMPTY]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
 721    (((repeat_tactic 1 9 (((use_arg_then2 ("IN_INSERT", [IN_INSERT]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("Geomdetail.CARD3", [Geomdetail.CARD3]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 722    ((DISJ1_TAC) THEN (split_tac));
 723    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE Collect_geom2.CAYLEYR_5POINTS))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0:real^3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("y", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 724    ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`vec 0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("DIST_0", [DIST_0]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_POW_2", [REAL_POW_2]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("y", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))));
 725    (((((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("norm_reflection", [norm_reflection]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("dist_reflection_special", [dist_reflection_special]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("DOT_CROSS_SELF", [DOT_CROSS_SELF]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 726    ((repeat_tactic 1 9 (((use_arg_then2 ("dist", [dist]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_ABS_NORM", [REAL_ABS_NORM]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("REAL_ABS_NORM", [REAL_ABS_NORM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`u - v:real^3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LT_SQUARE_ABS", [REAL_LT_SQUARE_ABS]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("dist", [dist]))(gsym_then (thm_tac (new_rewrite [] [])))))));
 727    ((((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dist_reflection_lemma", [dist_reflection_lemma]))(thm_tac (new_rewrite [] [])))));
 728    ((fun arg_tac -> arg_tac (Arg_term (`w cross w'`))) (term_tac (set_tac "n")));
 729    ((fun arg_tac -> arg_tac (Arg_term (`~(n = vec 0)`))) (term_tac (have_gen_tac [](move ["n0"]))));
 730    ((((use_arg_then2 ("n_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("CROSS_EQ_0", [CROSS_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))));
 731    ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_not_coplanar", [fully_surrounded_not_coplanar])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("Planarity.notcoplanar_imp_notcollinear_fan", [Planarity.notcoplanar_imp_notcollinear_fan])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 732    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`&0 < v dot n /\ u dot n < &0`))) (term_tac (have_gen_tac [](move ["ineqs"])))));
 733    ((fun arg_tac -> arg_tac (Arg_term (`&4 * _`))) (term_tac (set_tac "t")));
 734    ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`t < &0`))) (term_tac (have_gen_tac []ALL_TAC)))) ((arith_tac) THEN (done_tac)));
 735    ((((use_arg_then2 ("t_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LT_NEG", [REAL_LT_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_NEG_0", [REAL_NEG_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_RMUL", [REAL_NEG_RMUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LT_MUL", [REAL_LT_MUL]))(thm_tac (new_rewrite [] [])))));
 736    ((THENL_FIRST) (((((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_LMUL", [REAL_NEG_LMUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_RMUL", [REAL_NEG_RMUL]))(thm_tac (new_rewrite [] []))))) THEN (split_tac)) ((arith_tac) THEN (done_tac)));
 737    ((repeat_tactic 1 9 (((use_arg_then2 ("REAL_LT_MUL", [REAL_LT_MUL]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("REAL_LT_INV", [REAL_LT_INV]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("DOT_POS_LT", [DOT_POS_LT]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 738    ((((use_arg_then2 ("ineqs", [])) (disch_tac [])) THEN (clear_assumption "ineqs") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 739    ((((use_arg_then2 ("n_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("fully_surrounded_dot_cross", [fully_surrounded_dot_cross]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
 740    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fan_split_fan_face", [fan_split_fan_face])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 741    ((((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))));
 742    (BETA_TAC THEN (case THEN (move ["fan2"])) THEN (case THEN (move ["dart2_eq"])) THEN (move ["f_surr2"]));
 743    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`&0 < w' dot (w cross u)`))) (term_tac (have_gen_tac []ALL_TAC))));
 744    (((((use_arg_then2 ("CROSS_SKEW", [CROSS_SKEW]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_RNEG", [DOT_RNEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_SYM", [DOT_SYM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Trigonometry1.cross_triple", [Trigonometry1.cross_triple]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DOT_SYM", [DOT_SYM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_GT0", [REAL_NEG_GT0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 745    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`u = sigma_fan (vec 0) V ({w,w'} INSERT E) w' w`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
 746    (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_dot_cross", [fully_surrounded_dot_cross])) (fun fst_arg -> (use_arg_then2 ("fan2", [fan2])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_INSERT", [IN_INSERT]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 747    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE n_split_fan_face))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["eq1"]) THEN (move ["_"])))));
 748    ((((use_arg_then2 ("eq1", [])) (disch_tac [])) THEN (clear_assumption "eq1") THEN BETA_TAC) THEN (((((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("n_fan_pair", [n_fan_pair]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("u_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 749 ];;
 750 (Sections.add_section_hyp "subV" (`V SUBSET ball_annulus`));;
 751
 752 (* Lemma fully_surrounded_tau_eq_tauq *)
 753 let fully_surrounded_tau_eq_tauq = Sections.section_proof ["v";"w"]
 754 `v,w IN dart_of_fan (V,E)
 755         /\ CARD (face (hypermap_of_fan (V,E)) (v,w)) = 4
 756         ==>     let w' = sigma_fan (vec 0) V E v w in
 757                 let u = sigma_fan (vec 0) V E w' v in
 758                 let y1 = norm v in
 759                 let y2 = norm w in
 760                 let y3 = norm w' in
 761                 let y4 = dist(w,w') in
 762                 let y5 = dist(v,w') in
 763                 let y6 = dist(v,w) in
 764                 let y7 = norm u in
 765                 let y8 = dist(w',u) in
 766                 let y9 = dist(w,u) in
 767         tauVEF (V,E,face (hypermap_of_fan (V,E)) (v,w)) = tauq y1 y2 y3 y4 y5 y6 y7 y8 y9`
 768 [
 769    ((BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card4"])))) THEN (repeat_tactic 11 0 ((CONV_TAC let_CONV))));
 770    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fan_split_fan_face", [fan_split_fan_face])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 771    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE face_split_fan_face_explicit))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 772    ((THENL_FIRST) (((((use_arg_then2 ("card4", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `4 - 1 = 3`)))(thm_tac (new_rewrite [] []))))) THEN (ANTS_TAC)) ((arith_tac) THEN (done_tac)));
 773    (((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] []))));
 774    ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
 775    ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E w' v`))) (term_tac (set_tac "w2")));
 776    ((fun arg_tac -> arg_tac (Arg_term (`_ INSERT E`))) (term_tac (set_tac "E2")));
 777    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E2)`))) (term_tac (set_tac "H2")));
 778    (BETA_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["cards_eq"])) THEN (case THEN (move ["in_face"])) THEN (move ["neqs"]) THEN (case THEN (move ["fan2"])) THEN (case THEN (move ["dart2_eq"])) THEN (move ["f_surr2"]));
 779    ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart_of_fan (V,E2) /\ w',w IN dart_of_fan (V,E2)`))) (term_tac (have_gen_tac [](move ["all_in2"]))));
 780    (((((use_arg_then2 ("dart2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_INSERT", [IN_INSERT]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("vw_in", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 781    ((THENL_FIRST) (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE tau_split_fan_face_add))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) ((((use_arg_then2 ("card4", []))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)));
 782    ((((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("E2_def", []))(thm_tac (new_rewrite [] [])))));
 783    ((repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE fully_surrounded_tau_eq_taum)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 784    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E)`))) (term_tac (set_tac "H")));
 785    ((fun arg_tac -> arg_tac (Arg_term (`split_fan_face (V,E) (v,w) = (V,E2)`))) (term_tac (have_gen_tac [](move ["split_eq"]))));
 786    (((((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("E2_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 787    ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E2 v w = w'`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
 788    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`n_fan_pair (V,E2) (v,w) = n_fan_pair (V,E) (v,w)`))) (term_tac (have_gen_tac []ALL_TAC))));
 789    ((((repeat_tactic 1 9 (((use_arg_then2 ("n_fan_pair", [n_fan_pair]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 790    ((((use_arg_then2 ("split_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("n_split_fan_face_eq1", [n_split_fan_face_eq1])) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("neqs", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac));
 791    (((((use_arg_then2 ("split_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 792    ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E2 w' w = w2`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
 793    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`n_fan_pair (V,E2) (w',w) = n_fan_pair (V,E) (w',v)`))) (term_tac (have_gen_tac []ALL_TAC))));
 794    ((((repeat_tactic 1 9 (((use_arg_then2 ("n_fan_pair", [n_fan_pair]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w2_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 795    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE n_split_fan_face))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 796    ((((((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card4", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `3 < 4`)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("split_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 797    (((((use_arg_then2 ("Sphere.tauq", [Sphere.tauq]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("taum_sym", [taum_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`norm w2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 798 ];;
 799
 800 (* Finalization of the section EnclosedTauq *)
 801 let taum_sym = Sections.finalize_theorem taum_sym;;
 802 let fully_surrounded_enclosed = Sections.finalize_theorem fully_surrounded_enclosed;;
 803 let fully_surrounded_tau_eq_tauq = Sections.finalize_theorem fully_surrounded_tau_eq_tauq;;
 804 Sections.end_section "EnclosedTauq";;
 805
 806 (* Section Contravening *)
 807 Sections.begin_section "Contravening";;
 808 (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
 809 (Sections.add_section_hyp "contrV" (`contravening V`));;
 810
 811 (* Let fanV *)
 812 Sections.add_section_lemma "fanV" (Sections.section_proof []
 813 `FAN (vec 0,V,ESTD V)`
 814 [
 815    (((fun arg_tac -> (use_arg_then2 ("CONTRAVENING_FAN", [CONTRAVENING_FAN])) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
 816 ]);;
 817
 818 (* Let f_surr *)
 819 Sections.add_section_lemma "f_surr" (Sections.section_proof []
 820 `fully_surrounded (V,ESTD V)`
 821 [
 822    (((fun arg_tac -> (use_arg_then2 ("CONTRAVENING_IMP_FULLY_SURROUNDED", [CONTRAVENING_IMP_FULLY_SURROUNDED])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
 823 ]);;
 824
 825 (* Let dart1_eq *)
 826 Sections.add_section_lemma "dart1_eq" (Sections.section_proof []
 827 `dart_of_fan (V,ESTD V) = dart1_of_fan (V,ESTD V)`
 828 [
 829    (((fun arg_tac -> (use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
 830 ]);;
 831
 832 (* Lemma contravening_non_triangular_face_dist *)
 833 let contravening_non_triangular_face_dist = Sections.section_proof ["v";"w"]
 834 `v,w IN dart_of_fan (V,ESTD V)
 835         /\ 3 < CARD (face (hypermap_of_fan (V,ESTD V)) (v,w))
 836         ==>     let w' = sigma_fan (vec 0) V (ESTD V) v w in
 837                 let y1 = norm v in
 838                 let y2 = norm w in
 839                 let y3 = norm w' in
 840                 let y4 = dist (w,w') in
 841                 let y5 = dist (v,w') in
 842                 let y6 = dist (v,w) in
 843                         (&2 <= y1 /\ y1 <= &2 * h0) /\
 844                         (&2 <= y2 /\ y2 <= &2 * h0) /\
 845                         (&2 <= y3 /\ y3 <= &2 * h0) /\
 846                         (&2 * h0 <= y4 /\ y4 <= &4 * h0) /\
 847                         (&2 <= y5 /\ y5 <= &2 * h0) /\
 848                         (&2 <= y6 /\ y6 <= &2 * h0)`
 849 [
 850    ((BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card_gt3"])))) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))));
 851    ((((use_arg_then2 ("h0", [h0]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `&2 * #1.26 = #2.52 /\ &2 = #2.0`)))(thm_tac (new_rewrite [] []))))));
 852    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (V,ESTD V)`))) (term_tac (have_gen_tac [](move ["vw_in1"])))) ((((use_arg_then2 ("dart1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 853    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sigma_fan_inV", [sigma_fan_inV])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["w'_in"])));
 854    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sigma_in_dart1", [sigma_in_dart1])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["vw'_in"])));
 855    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sigma_fan_not_fixed", [sigma_fan_not_fixed])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["w'_neq_w"])));
 856    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_diag_not_in_dart", [fully_surrounded_diag_not_in_dart])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card_gt3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["not_diag"])));
 857    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["v_in"]) THEN (move ["w_in"])))));
 858    ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _1 V _2 v w`))) (term_tac (set_tac "w'")));
 859    ((repeat_tactic 1 9 (((use_arg_then2 ("Trigonometry1.DIST_L_ZERO", [Trigonometry1.DIST_L_ZERO]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("CONTRAVENING_DIST", [CONTRAVENING_DIST])) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))));
 860    (((((use_arg_then2 ("andbC", [andbC]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 4 (((fun arg_tac -> (use_arg_then2 ("CONTRAVENING_DART_DIST", [CONTRAVENING_DART_DIST])) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))))) THEN (split_tac));
 861    ((((use_arg_then2 ("not_diag", [])) (disch_tac [])) THEN (clear_assumption "not_diag") THEN BETA_TAC) THEN ((((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_of_fan", [dart1_of_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("NOT_EXISTS_THM", [NOT_EXISTS_THM]))(thm_tac (new_rewrite [] [])))))));
 862    ((((fun arg_tac -> (fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)) THEN BETA_TAC) THEN ((simp_tac) THEN (((use_arg_then2 ("IN_ESTD", [IN_ESTD]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_neq_w", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (arith_tac) THEN (done_tac));
 863    (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("DIST_TRIANGLE_LE", [DIST_TRIANGLE_LE])) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 864    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`&4 * #1.26 = #2.52 + #2.52`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
 865    (((((use_arg_then2 ("REAL_LE_ADD2", [REAL_LE_ADD2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DIST_SYM", [DIST_SYM]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("DIST_SYM", [DIST_SYM])) (fun fst_arg -> (use_arg_then2 ("w'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("CONTRAVENING_DART_DIST", [CONTRAVENING_DART_DIST])) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 866 ];;
 867
 868 (* Section Ineqs *)
 869 Sections.begin_section "Ineqs";;
 870 (Sections.add_section_hyp "ineqs" (`kcblrqc_ineq_def`));;
 871
 872 (* Lemma non_triangular_face_azim_dart_bound *)
 873 let non_triangular_face_azim_dart_bound = Sections.section_proof ["d"]
 874 `d IN dart_of_fan (V,ESTD V)
 875         /\ 3 < CARD (face (hypermap_of_fan (V,ESTD V)) d)
 876         ==> #1.15 < azim_dart (V,ESTD V) d`
 877 [
 878    (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (case THEN ((move ["vw_in"]) THEN (move ["card_gt3"]))));
 879    ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE CONTRAVENING_AZIM_DART_EQ_DIH_Y)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("real_gt", [real_gt]))(gsym_then (thm_tac (new_rewrite [] []))))));
 880    ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _1 V _2 v w`))) (term_tac (set_tac "w'")));
 881    (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Tame_inequalities.DIH_Y_INEQ))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`norm v`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`norm w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`norm w'`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dist (w,w')`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dist (v,w')`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dist (v,w)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN (ANTS_TAC));
 882    ((((use_arg_then2 ("ineqs", [])) (disch_tac [])) THEN (clear_assumption "ineqs") THEN BETA_TAC) THEN ((((use_arg_then2 ("kcblrqc_ineq_def", [kcblrqc_ineq_def]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 883    (((((use_arg_then2 ("INEQ_ALT", [INEQ_ALT]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL ALL)))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (ANTS_TAC));
 884    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`#2.0 = &2 /\ #2.52 = &2 * h0 /\ #5.04 = &4 * h0`))) (term_tac (have_gen_tac [](move ["eqs"])))) ((((use_arg_then2 ("h0", [h0]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)));
 885    (((repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 12 0 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE contravening_non_triangular_face_dist))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card_gt3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 886    (((((use_arg_then2 ("REAL_NOT_LT", [REAL_NOT_LT]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE fully_surrounded_delta_pos))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 887 ];;
 888
 889 (* Finalization of the section Ineqs *)
 890 let non_triangular_face_azim_dart_bound = Sections.finalize_theorem non_triangular_face_azim_dart_bound;;
 891 Sections.end_section "Ineqs";;
 892
 893 (* Finalization of the section Contravening *)
 894 let contravening_non_triangular_face_dist = Sections.finalize_theorem contravening_non_triangular_face_dist;;
 895 let non_triangular_face_azim_dart_bound = Sections.finalize_theorem non_triangular_face_azim_dart_bound;;
 896 Sections.end_section "Contravening";;
 897
 898 (* Close the module *)
 899 end;;