flyspeck_needs "../formal_lp/hypermap/ssreflect/add_triangle-compiled.hl";;

(* Module Tame_lemmas*)
module Tame_lemmas = struct

let reflection = new_definition `reflection n x = x - (&2 * (x dot n) / (n dot n)) % n`;;
let kcblrqc_ineq_tml = 
  let has_id = (fun t -> not(intersect ["KCBLRQC"] (Ineq.flypaper_ids t) = [])) in
  let extra_ids = [
	"3287695934"; 
	"6988401556"; 
	"3862621143 back"; 
	"3862621143 front";
	"3862621143 side";
	"4240815464 a reduced";
	"6944699408 a reduced";
	"7043724150 a reduced v2";
  ] in
  let idl = (filter (fun t -> has_id t or mem t.idv extra_ids) !Ineq.ineqs) in
  let tml = map (fun t -> t.ineq) idl in
    end_itlist (curry mk_conj) tml;;
let kcblrqc_ineq_def = new_definition
	(mk_eq (`kcblrqc_ineq_def:bool`, kcblrqc_ineq_tml));;
open Tame_general;;
open Add_triangle;;
open Fan_defs;;
open Pack_defs;;
open Hypermap;;
open Hypermap_and_fan;;
open Hypermap_iso;;
open Ssrbool;;
open Ssrnat;;

(* Section Reflection *)
Sections.begin_section "Reflection";;
let VECTOR_MUL_RZERO = GEN_ALL VECTOR_MUL_RZERO;;
let VECTOR_SUB_RZERO = GEN_ALL VECTOR_SUB_RZERO;;
let VECTOR_SUB_RDISTRIB = GEN_ALL VECTOR_SUB_RDISTRIB;;
let VECTOR_ADD_RDISTRIB = GEN_ALL VECTOR_ADD_RDISTRIB;;
let VECTOR_SUB_LDISTRIB = GEN_ALL VECTOR_SUB_LDISTRIB;;
(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`))));;

(* Lemma reflection_at0 *)
let reflection_at0 = Sections.section_proof ["x"]
`reflection (vec 0) x = x`
[
   (((((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));
];;

(* Lemma reflection_eq *)
let reflection_eq = Sections.section_proof ["n";"x"]
`x dot n = &0 ==> reflection n x = x`
[
   ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
   (((((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));
];;

(* Lemma reflection_eq2 *)
let reflection_eq2 = Sections.section_proof ["n";"x"]
`reflection n x = x <=> x dot n = &0`
[
   ((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)));
   ((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)));
   ((((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 [] [])))));
   (((((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));
];;

(* Lemma reflection0 *)
let reflection0 = Sections.section_proof ["n"]
`reflection n (vec 0) = vec 0`
[
   (((((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));
];;

(* Lemma reflection_sub *)
let reflection_sub = Sections.section_proof ["n";"x";"y"]
`reflection n (x - y) = reflection n x - reflection n y`
[
   ((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 [] [])))));
   ((((use_arg_then2 ("VECTOR_SUB_RDISTRIB", [VECTOR_SUB_RDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (VECTOR_ARITH_TAC) THEN (done_tac));
];;

(* Lemma reflection_add *)
let reflection_add = Sections.section_proof ["n";"x";"y"]
`reflection n (x + y) = reflection n x + reflection n y`
[
   ((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 [] [])))));
   ((((use_arg_then2 ("VECTOR_ADD_RDISTRIB", [VECTOR_ADD_RDISTRIB]))(thm_tac (new_rewrite [] [])))) THEN (VECTOR_ARITH_TAC) THEN (done_tac));
];;

(* Lemma reflection_cmul *)
let reflection_cmul = Sections.section_proof ["n";"c";"x"]
`reflection n (c % x) = c % reflection n x`
[
   ((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 [] [])))));
   (((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));
];;

(* Lemma norm_reflection *)
let norm_reflection = Sections.section_proof ["n";"x"]
`norm (reflection n x) = norm x`
[
   ((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)));
   ((((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 [] [])))));
   ((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)));
   ((((use_arg_then2 ("DOT_EQ_0", [DOT_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma dist_reflection *)
let dist_reflection = Sections.section_proof ["n";"x";"y"]
`dist (reflection n x, reflection n y) = dist (x, y)`
[
   (((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));
];;

(* Lemma dist_reflection_special *)
let dist_reflection_special = Sections.section_proof ["n";"x";"y"]
`y dot n = &0 ==> dist (reflection n x, y) = dist (x, y)`
[
   (((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));
];;

(* Lemma reflection_dot *)
let reflection_dot = Sections.section_proof ["n";"x"]
`(reflection n x) dot n = --(x dot n)`
[
   ((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)));
   ((((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 [] [])))));
   ((((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));
];;

(* Lemma dist_reflection_lemma *)
let dist_reflection_lemma = Sections.section_proof ["n";"x";"y"]
`dist (reflection n x, y) pow 2
	= dist (x, y) pow 2 + &4 * ((y dot n) * (x dot n)) / (n dot n)`
[
   (((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 (((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));
   (((use_arg_then2 ("Collect_geom.DIST_POW2_DOT", [Collect_geom.DIST_POW2_DOT]))(thm_tac (new_rewrite [] []))));
   ((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] [])))))));
   ((((use_arg_then2 ("reflection", [reflection]))(thm_tac (new_rewrite [] [])))) THEN (VECTOR_ARITH_TAC) THEN (done_tac));
   ((fun arg_tac -> arg_tac (Arg_term (`&2 * _`))) (term_tac (set_tac "a")));
   ((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)));
   ((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 [] [])))))));
   (((((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));
   ((((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 [] [])))));
   ((((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 [] []))))));
   ((((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 [] []))))));
   ((CONV_TAC REAL_FIELD) THEN (done_tac));
];;

(* Finalization of the section Reflection *)
let reflection_at0 = Sections.finalize_theorem reflection_at0;;
let reflection_eq = Sections.finalize_theorem reflection_eq;;
let reflection_eq2 = Sections.finalize_theorem reflection_eq2;;
let reflection0 = Sections.finalize_theorem reflection0;;
let reflection_sub = Sections.finalize_theorem reflection_sub;;
let reflection_add = Sections.finalize_theorem reflection_add;;
let reflection_cmul = Sections.finalize_theorem reflection_cmul;;
let norm_reflection = Sections.finalize_theorem norm_reflection;;
let dist_reflection = Sections.finalize_theorem dist_reflection;;
let dist_reflection_special = Sections.finalize_theorem dist_reflection_special;;
let reflection_dot = Sections.finalize_theorem reflection_dot;;
let dist_reflection_lemma = Sections.finalize_theorem dist_reflection_lemma;;
Sections.end_section "Reflection";;

(* Section Misc *)
Sections.begin_section "Misc";;
(Sections.add_section_type (mk_var ("v", (`:real^3`))));;

(* Lemma delta_y_pos *)
let delta_y_pos = Sections.section_proof ["v";"w";"w'"]
`let y1 = norm v in
	 let y2 = norm w in
	 let y3 = norm w' in
	 let y4 = dist (w,w') in
	 let y5 = dist (v,w') in
	 let y6 = dist (v,w) in
		&0 <= delta_y y1 y2 y3 y4 y5 y6`
[
   (repeat_tactic 1 9 ((CONV_TAC let_CONV)));
   ((((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 [] [])))))));
   ((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));
   ((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));
];;

(* Lemma quadratic_root_plus_works *)
let quadratic_root_plus_works = Sections.section_proof ["a";"b";"c"]
`~(a = &0) /\ &0 <= b pow 2 - &4 * a * c ==>
	let x = quadratic_root_plus (a,b,c) in
		a * x pow 2 + b * x + c = &0`
[
   ((BETA_TAC THEN (move ["ineqs"])) THEN (CONV_TAC let_CONV));
   (((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 [] []))));
   ((((use_arg_then2 ("Sphere.quadratic_root_plus", [Sphere.quadratic_root_plus]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
];;

(* Lemma quadratic_root_plus_eq *)
let quadratic_root_plus_eq = Sections.section_proof ["a";"b";"c";"x"]
`&0 < a /\ &0 <= b pow 2 - &4 * a * c 
	/\ &0 <= b /\ (a * x pow 2 + b * x + c = &0) /\ &0 <= x
	==> quadratic_root_plus (a,b,c) = x`
[
   (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"]));
   ((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)));
   ((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));
   ((((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 [] [])))));
   ((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"]));
   ((fun arg_tac -> arg_tac (Arg_term (`x <= &0`))) (term_tac (have_gen_tac []ALL_TAC)));
   (((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] []))));
   ((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)));
   ((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 [] [])))));
   ((((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 [] [])))));
   ((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)));
   ((((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));
   ((((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));
   ((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)));
   (BETA_TAC THEN (move ["x_eq0"]));
   ((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)));
   ((((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 [] [])))));
   (((((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));
];;

(* Lemma quadratic_root_plus_gt_eq *)
let quadratic_root_plus_gt_eq = Sections.section_proof ["a";"b";"c";"x";"y"]
`&0 < a /\ &0 <= b pow 2 - &4 * a * c
	/\ a * x pow 2 + b * x + c = &0 /\ a * y pow 2 + b * y + c = &0 /\ y < x
	==> quadratic_root_plus (a,b,c) = x`
[
   (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"]));
   ((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)));
   ((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"])));
   ((((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 [] [])))))));
   (((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"]));
   ((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)));
   ((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)));
   ((((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));
];;

(* Lemma quadratic_root_plus_disc0_eq *)
let quadratic_root_plus_disc0_eq = Sections.section_proof ["a";"b";"c";"x"]
`~(a = &0) /\ b pow 2 - &4 * a * c = &0 
	/\ a * x pow 2 + b * x + c = &0
	==> quadratic_root_plus (a,b,c) = x`
[
   (BETA_TAC THEN (case THEN (move ["a_neq0"])) THEN (case THEN (move ["disc0"])) THEN (move ["x_root"]));
   (((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));
   (((((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));
   ((((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 [] [])))));
   (((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)));
   ((((((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));
];;

(* Finalization of the section Misc *)
let delta_y_pos = Sections.finalize_theorem delta_y_pos;;
let quadratic_root_plus_works = Sections.finalize_theorem quadratic_root_plus_works;;
let quadratic_root_plus_eq = Sections.finalize_theorem quadratic_root_plus_eq;;
let quadratic_root_plus_gt_eq = Sections.finalize_theorem quadratic_root_plus_gt_eq;;
let quadratic_root_plus_disc0_eq = Sections.finalize_theorem quadratic_root_plus_disc0_eq;;
Sections.end_section "Misc";;

(* Section FullySurrounded *)
Sections.begin_section "FullySurrounded";;
(Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
(Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));;
(Sections.add_section_hyp "fanV" (`FAN (vec 0,V,E)`));;
(Sections.add_section_hyp "f_surr" (`fully_surrounded (V,E)`));;

(* Let dart1_eq *)
Sections.add_section_lemma "dart1_eq" (Sections.section_proof []
`dart_of_fan (V,E) = dart1_of_fan (V,E)`
[
   ((((use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
]);;

(* Let confV *)
Sections.add_section_lemma "confV" (Sections.section_proof []
`conforming_fan (vec 0,V,E)`
[
   ((((use_arg_then2 ("fully_surrounded_imp_conforming", [fully_surrounded_imp_conforming]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
]);;

(* Let dartH *)
Sections.add_section_lemma "dartH" (Sections.section_proof []
`dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E)`
[
   ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
]);;

(* Lemma dart_leads_into_eq1 *)
let dart_leads_into_eq1 = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E)
	==> dart_leads_into (vec 0) V E v w 
		= dartset_leads_into_fan (vec 0) V E 
			(IMAGE (ext_dart (V,E)) (face (hypermap_of_fan (V,E)) (v,w)))`
[
   (BETA_TAC THEN (move ["vw_in"]));
   ((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"])));
   ((fun arg_tac -> arg_tac (Arg_term (`ext_dart _`))) (term_tac (set_tac "h")));
   ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
   ((((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)));
   ((fun arg_tac -> arg_tac (Arg_term (`face _1 _2`))) (term_tac (set_tac "f1")));
   ((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 [] [])))));
   (((((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));
   ((((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 [] []))))));
   (((((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"]));
   ((((use_arg_then2 ("fully_surrounded_card_set_of_edge1", [fully_surrounded_card_set_of_edge1]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;

(* Lemma dart_leads_into_same *)
let dart_leads_into_same = Sections.section_proof ["f";"v";"w";"x";"y"]
`f IN face_set (hypermap_of_fan (V,E)) 
	/\ (v,w) IN f /\ (x,y) IN f
	==> dart_leads_into (vec 0) V E v w = dart_leads_into (vec 0) V E x y`
[
   (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"]))));
   ((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"]))));
   (((((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));
   ((repeat_tactic 1 9 (((use_arg_then2 ("dart_leads_into_eq1", [dart_leads_into_eq1]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
   (((((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));
];;

(* Lemma fully_surrounded_sol *)
let fully_surrounded_sol = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E)
   ==> sol (vec 0) (dart_leads_into (vec 0) V E v w)
	= &2 * pi + sum (face (hypermap_of_fan (V,E)) (v,w)) (\x. azim_dart (V,E) x - pi)`
[
   (BETA_TAC THEN (move ["vw_in"]));
   ((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"])));
   ((((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 [] []))))));
   (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 ["_"]));
   ((((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 [] [])))));
   (((((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));
   ((congr_tac (`_1 + _2:real`)) THEN ((TRY done_tac)));
   ((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"]))));
   (((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));
   (((use_arg_then2 ("SUM_IMAGE", [SUM_IMAGE]))(thm_tac (new_rewrite [] []))));
   (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)))));
   (((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((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"])));
   (((((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));
];;

(* Lemma fully_surrounded_sum_sol *)
let fully_surrounded_sum_sol = Sections.section_proof []
`sum (face_set (hypermap_of_fan (V,E)))
	(\f. sol (vec 0) (dartset_leads_into_fan (vec 0) V E  (IMAGE (ext_dart (V,E)) f))) 
	= &4 * pi`
[
   ((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"])));
   ((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));
   ((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 [] []))))));
   ((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));
   (BETA_TAC THEN (move ["f1"]) THEN (move ["f2"]));
   (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 [] [])))))));
   ((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)));
   ((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 [] []))))));
   (((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));
];;

(* Lemma fully_surrounded_not_coplanar *)
let fully_surrounded_not_coplanar = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E)
	==> ~(coplanar {vec 0, v, w, sigma_fan (vec 0) V E v w})`
[
   ((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"])));
   ((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"])));
   ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _1 V _2 v w`))) (term_tac (set_tac "w'")));
   ((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 [] [])))))));
   ((((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));
   ((((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)));
   ((((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 [] [])))));
   ((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 [] [])))));
   ((((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));
];;

(* Lemma fully_surrounded_delta_pos *)
let fully_surrounded_delta_pos = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E) ==>
		let w' = sigma_fan (vec 0) V E v w in
		let y1 = norm v in
		let y2 = norm w in
		let y3 = norm w' in
		let y4 = dist (w,w') in
		let y5 = dist (v,w') in
		let y6 = dist (v,w) in
			&0 < delta_y y1 y2 y3 y4 y5 y6`
[
   (((((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))));
   ((((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 [] [])))))));
   (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom2.POS_EQ_NOT_COPLANANR)))(thm_tac (new_rewrite [] []))));
   ((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)));
   (((use_arg_then2 ("fully_surrounded_not_coplanar", [fully_surrounded_not_coplanar])) (disch_tac [])) THEN (clear_assumption "fully_surrounded_not_coplanar") THEN (exact_tac));
];;

(* Lemma fully_surrounded_azim_eq_dih_y *)
let fully_surrounded_azim_eq_dih_y = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E) ==>
	 let w' = sigma_fan (vec 0) V E v w in
	 let y1 = norm v in
	 let y2 = norm w in
	 let y3 = norm w' in
	 let y4 = dist (w,w') in
	 let y5 = dist (v,w') in
	 let y6 = dist (v,w) in
		azim_dart (V,E) (v,w) = dih_y y1 y2 y3 y4 y5 y6`
[
   ((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"])));
   ((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"])));
   ((((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)));
   ((((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)));
   ((((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))));
   ((((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)));
   ((repeat_tactic 1 9 (((use_arg_then2 ("Trigonometry1.DIST_L_ZERO", [Trigonometry1.DIST_L_ZERO]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;

(* Lemma fully_surrounded_sol_eq_sol_y *)
let fully_surrounded_sol_eq_sol_y = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E) /\
	CARD (face (hypermap_of_fan (V,E)) (v,w)) = 3 ==>
		 let w' = sigma_fan (vec 0) V E v w in
		 let y1 = norm v in
		 let y2 = norm w in
		 let y3 = norm w' in
		 let y4 = dist (w,w') in
		 let y5 = dist (v,w') in
		 let y6 = dist (v,w) in
	sol (vec 0) (dart_leads_into (vec 0) V E v w) = sol_y y1 y2 y3 y4 y5 y6`
[
   ((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"])));
   ((((use_arg_then2 ("fully_surrounded_sol", [fully_surrounded_sol]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
   ((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"])))));
   ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
   ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
   ((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"]))));
   ((((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));
   ((fun arg_tac -> arg_tac (Arg_term (`~(v = w) /\ ~(w' = v) /\ ~(w = w')`))) (term_tac (have_gen_tac [](move ["neqs"]))));
   (((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));
   ((((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)));
   ((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));
   ((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 [] []))))));
   (((((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));
];;

(* Lemma tauVEF_alt1 *)
let tauVEF_alt1 = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E)
	==> let f = face (hypermap_of_fan (V,E)) (v,w) in
		tauVEF (V,E,f) = sol (vec 0) (dart_leads_into (vec 0) V E v w)
		  + (&2 - &(CARD f)) * sol0
		  - sol0 / pi * sum f (\x. azim_dart (V,E) x * (lmfun (h_dart x) - &1))`
[
   ((BETA_TAC THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
   ((((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)));
   ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
   ((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"])));
   (((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 [] []))));
   (((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));
];;

(* Lemma tauVEF_alt2 *)
let tauVEF_alt2 = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E)
	==> let f = face (hypermap_of_fan (V,E)) (v,w) in
	  tauVEF (V,E,f) = sol (vec 0) (dart_leads_into (vec 0) V E v w) * (&1 + sol0 / pi) 
			- sol0 / pi * sum f (\x. azim_dart (V,E) x * lmfun (h_dart x))`
[
   ((BETA_TAC THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
   ((((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)));
   ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
   ((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"])));
   ((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)));
   ((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)));
   ((((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));
];;

(* Lemma tauVEF_alt2_alt *)
let tauVEF_alt2_alt = Sections.section_proof ["f"]
`f IN face_set (hypermap_of_fan (V,E))
   ==> tauVEF (V,E,f) 
	= sol (vec 0) (dartset_leads_into_fan (vec 0) V E  (IMAGE (ext_dart (V,E)) f)) 
		* (&1 + sol0 / pi) 
		- sol0 / pi * sum f (\x. azim_dart (V,E) x * lmfun (h_dart x))`
[
   (((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"])));
   (((((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));
];;

(* Lemma tauVEF_alt3 *)
let tauVEF_alt3 = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E)
	==> let f = face (hypermap_of_fan (V,E)) (v,w) in
	tauVEF (V,E,f) = sum f (\x. (&1 + sol0 / pi * (&1 - lmfun (h_dart x))) 
	* azim_dart (V,E) x - pi - sol0) + &2 * (pi + sol0)`
[
   ((BETA_TAC THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
   ((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)));
   ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
   ((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"])));
   ((((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)));
   ((((use_arg_then2 ("Tame_defs.tauVEF", [Tame_defs.tauVEF]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
];;

(* Lemma sum_tauVEF_upper_bound *)
let sum_tauVEF_upper_bound = Sections.section_proof []
`&12 <= scriptL V ==>
	 sum (face_set (hypermap_of_fan (V,E))) (\f. tauVEF (V,E,f)) 
		<= &4 * pi - &20 * sol0`
[
   ((((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"]));
   ((((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 [] [])))));
   (((use_arg_then2 ("fully_surrounded_sum_sol", [fully_surrounded_sum_sol]))(thm_tac (new_rewrite [] []))));
   ((((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)));
   ((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 [] [])))))));
   ((((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));
   ((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 [] [])))));
   (((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 [] []))));
   ((((use_arg_then2 ("ineq", [])) (disch_tac [])) THEN (clear_assumption "ineq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
];;

(* Lemma fully_surrounded_dot_cross *)
let fully_surrounded_dot_cross = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E)
	==> &0 < v dot (w cross sigma_fan (vec 0) V E v w)`
[
   (BETA_TAC THEN (move ["vw_in"]));
   ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
   ((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));
   ((((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"])));
   (((((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"]));
   (((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))));
   ((((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 [] [])))));
   ((((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));
   ((((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)));
   ((((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));
];;

(* Section BallAnnulus *)
Sections.begin_section "BallAnnulus";;
(Sections.add_section_hyp "subV" (`V SUBSET ball_annulus`));;

(* Let v_norm *)
Sections.add_section_lemma "v_norm" (Sections.section_proof ["v"]
`v IN V ==> norm v <= &2 * h0 /\ &2 <= norm v`
[
   ((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));
]);;

(* Lemma fully_surrounded_lnazim *)
let fully_surrounded_lnazim = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E) ==>
	 let w' = sigma_fan (vec 0) V E v w in
	 let y1 = norm v in
	 let y2 = norm w in
	 let y3 = norm w' in
	 let y4 = dist (w,w') in
	 let y5 = dist (v,w') in
	 let y6 = dist (v,w) in
		azim_dart (V,E) (v,w) * lmfun (h_dart (v,w)) = lnazim y1 y2 y3 y4 y5 y6`
[
   ((BETA_TAC THEN (move ["vw_in"])) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))));
   ((((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 [] []))))));
   (((((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));
];;

(* Lemma fully_surrounded_tau_eq_taum *)
let fully_surrounded_tau_eq_taum = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E)
	/\ CARD (face (hypermap_of_fan (V,E)) (v,w)) = 3
	==>	let w' = sigma_fan (vec 0) V E v w in
		let y1 = norm v in
		let y2 = norm w in
		let y3 = norm w' in
		let y4 = dist (w,w') in
		let y5 = dist (v,w') in
		let y6 = dist (v,w) in
		tauVEF (V,E,face (hypermap_of_fan (V,E)) (v,w)) = taum y1 y2 y3 y4 y5 y6`
[
   ((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"])));
   ((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"])))));
   ((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 ["_"])))));
   ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
   ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
   ((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"]))));
   ((((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));
   ((fun arg_tac -> arg_tac (Arg_term (`~(v = w) /\ ~(w' = v) /\ ~(w = w')`))) (term_tac (have_gen_tac [](move ["neqs"]))));
   (((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));
   ((((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 [] [])))));
   ((((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)));
   ((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));
   ((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 [] []))))));
   ((((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 [] [])))));
   (((((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));
];;

(* Finalization of the section BallAnnulus *)
let fully_surrounded_lnazim = Sections.finalize_theorem fully_surrounded_lnazim;;
let fully_surrounded_tau_eq_taum = Sections.finalize_theorem fully_surrounded_tau_eq_taum;;
Sections.end_section "BallAnnulus";;

(* Finalization of the section FullySurrounded *)
let dart_leads_into_eq1 = Sections.finalize_theorem dart_leads_into_eq1;;
let dart_leads_into_same = Sections.finalize_theorem dart_leads_into_same;;
let fully_surrounded_sol = Sections.finalize_theorem fully_surrounded_sol;;
let fully_surrounded_sum_sol = Sections.finalize_theorem fully_surrounded_sum_sol;;
let fully_surrounded_not_coplanar = Sections.finalize_theorem fully_surrounded_not_coplanar;;
let fully_surrounded_delta_pos = Sections.finalize_theorem fully_surrounded_delta_pos;;
let fully_surrounded_azim_eq_dih_y = Sections.finalize_theorem fully_surrounded_azim_eq_dih_y;;
let fully_surrounded_sol_eq_sol_y = Sections.finalize_theorem fully_surrounded_sol_eq_sol_y;;
let tauVEF_alt1 = Sections.finalize_theorem tauVEF_alt1;;
let tauVEF_alt2 = Sections.finalize_theorem tauVEF_alt2;;
let tauVEF_alt2_alt = Sections.finalize_theorem tauVEF_alt2_alt;;
let tauVEF_alt3 = Sections.finalize_theorem tauVEF_alt3;;
let sum_tauVEF_upper_bound = Sections.finalize_theorem sum_tauVEF_upper_bound;;
let fully_surrounded_dot_cross = Sections.finalize_theorem fully_surrounded_dot_cross;;
let fully_surrounded_lnazim = Sections.finalize_theorem fully_surrounded_lnazim;;
let fully_surrounded_tau_eq_taum = Sections.finalize_theorem fully_surrounded_tau_eq_taum;;
Sections.end_section "FullySurrounded";;

(* Section EnclosedTauq *)
Sections.begin_section "EnclosedTauq";;

(* Lemma taum_sym *)
let taum_sym = Sections.section_proof ["y1";"y2";"y3";"y4";"y5";"y6"]
`taum y1 y2 y3 y4 y5 y6 = taum y3 y2 y1 y6 y5 y4`
[
   ((use_arg_then2 ("Nonlinear_lemma.dih_y_sym", [Nonlinear_lemma.dih_y_sym])) (fun arg -> thm_tac MP_TAC arg THEN (move ["sym"])));
   ((((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 [] []))))));
   ((((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 [] [])))));
   ((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)));
   (((use_arg_then2 ("Sphere.sol_y", [Sphere.sol_y]))(gsym_then (thm_tac (new_rewrite [] [])))));
   ((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)));
   (((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));
];;
(Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
(Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));;
(Sections.add_section_hyp "fanV" (`FAN (vec 0,V,E)`));;
(Sections.add_section_hyp "f_surr" (`fully_surrounded (V,E)`));;

(* Let dart1_eq *)
Sections.add_section_lemma "dart1_eq" (Sections.section_proof []
`dart_of_fan (V,E) = dart1_of_fan (V,E)`
[
   ((((use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
]);;

(* Let dartH *)
Sections.add_section_lemma "dartH" (Sections.section_proof []
`dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E)`
[
   ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
]);;

(* Lemma fully_surrounded_enclosed *)
let fully_surrounded_enclosed = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E)
	==>	let w' = sigma_fan (vec 0) V E v w in
		let u = sigma_fan (vec 0) V E w' v in
		let y1 = norm v in
		let y2 = norm w in
		let y3 = norm w' in
		let y4 = dist(w,w') in
		let y5 = dist(v,w') in
		let y6 = dist(v,w) in
		let y7 = norm u in
		let y8 = dist(w',u) in
		let y9 = dist(w,u) in
	dist (v,u) = enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9`
[
   ((BETA_TAC THEN (move ["vw_in"])) THEN (repeat_tactic 11 0 ((CONV_TAC let_CONV))));
   ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
   ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E w' v`))) (term_tac (set_tac "u")));
   (((use_arg_then2 ("Enclosed.enclosed", [Enclosed.enclosed]))(thm_tac (new_rewrite [] []))));
   ((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));
   ((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 [] []))))));
   ((fun arg_tac -> arg_tac (Arg_term (`muR _1 _2 _3 _4 _5 _6 _7 _8 _9`))) (term_tac (set_tac "p")));
   (BETA_TAC THEN (move ["p0"]));
   (((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 [] []))))))));
   (((((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));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`?a b c x. (p = \x. a * x pow 2 + b * x + c) 
	/\ &0 < a /\ &0 <= b pow 2 - &4 * a * c 
	/\ (p (dist (x, v) * dist (x, v)) = &0 /\ dist (x, v) < dist (u, v) 
		\/ b pow 2 - &4 * a * c = &0)`))) (term_tac (have_gen_tac []ALL_TAC))));
   (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"]));
   ((((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 [] [])))));
   ((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"])]));
   (((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));
   (((((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));
   ((((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)));
   ((((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 [] []))))));
   ((((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)));
   (((((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));
   ((((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 [] [])))));
   ((fun arg_tac -> arg_tac (Arg_term (`ups_x _1 _2 _3`))) (term_tac (set_tac "a")));
   ((fun arg_tac -> arg_tac (Arg_term (`cayleytr _1 _2 _3 _4 _5 _6 _7 _8 _9 _10`))) (term_tac (set_tac "b")));
   ((fun arg_tac -> arg_tac (Arg_term (`cayleyR _1 _2 _3 _4 _5 _6 _7 _8 _9 _10`))) (term_tac (set_tac "c")));
   ((fun arg_tac -> arg_tac (Arg_term (`reflection (w cross w') u`))) (term_tac (set_tac "y")));
   (((((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));
   (((use_arg_then2 ("a_def", []))(gsym_then (thm_tac (new_rewrite [] [])))));
   ((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));
   (((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));
   (((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);
   ((((((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));
   (split_tac);
   ((((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 [] [])))));
   ((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 [] []))))));
   ((THENL_LAST) (repeat_tactic 1 9 (((use_arg_then2 ("REAL_LE_MUL", [REAL_LE_MUL]))(thm_tac (new_rewrite [] []))))) ((arith_tac) THEN (done_tac)));
   ((repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE delta_y_pos)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
   (((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"]));
   ((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 [] []))))));
   ((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 [] []))))));
   ((fun arg_tac -> arg_tac (Arg_term (`u = w`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
   (((((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));
   ((repeat_tactic 1 9 (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (DISJ2_TAC) THEN (DISJ2_TAC));
   ((((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 [] [])))))));
   ((((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 [] []))))));
   ((((use_arg_then2 ("DIMINDEX_3", [DIMINDEX_3]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
   (((fun arg_tac -> arg_tac (Arg_theorem ((GEN_ALL o CONJUNCT2) Collect_geom2.PER_SET4)))(thm_tac (new_rewrite [] []))));
   ((((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 [] [])))));
   (((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));
   ((DISJ1_TAC) THEN (split_tac));
   ((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));
   ((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 [] []))))));
   (((((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));
   ((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 [] [])))))));
   ((((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 [] [])))));
   ((fun arg_tac -> arg_tac (Arg_term (`w cross w'`))) (term_tac (set_tac "n")));
   ((fun arg_tac -> arg_tac (Arg_term (`~(n = vec 0)`))) (term_tac (have_gen_tac [](move ["n0"]))));
   ((((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 [] []))))));
   ((((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));
   (((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"])))));
   ((fun arg_tac -> arg_tac (Arg_term (`&4 * _`))) (term_tac (set_tac "t")));
   ((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)));
   ((((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 [] [])))));
   ((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)));
   ((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)));
   ((((use_arg_then2 ("ineqs", [])) (disch_tac [])) THEN (clear_assumption "ineqs") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
   ((((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 [] [])))));
   ((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));
   ((((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))));
   (BETA_TAC THEN (case THEN (move ["fan2"])) THEN (case THEN (move ["dart2_eq"])) THEN (move ["f_surr2"]));
   (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`&0 < w' dot (w cross u)`))) (term_tac (have_gen_tac []ALL_TAC))));
   (((((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));
   (((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 [] []))))))));
   (((((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));
   ((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 ["_"])))));
   ((((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));
];;
(Sections.add_section_hyp "subV" (`V SUBSET ball_annulus`));;

(* Lemma fully_surrounded_tau_eq_tauq *)
let fully_surrounded_tau_eq_tauq = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,E)
	/\ CARD (face (hypermap_of_fan (V,E)) (v,w)) = 4
	==>	let w' = sigma_fan (vec 0) V E v w in
		let u = sigma_fan (vec 0) V E w' v in
		let y1 = norm v in
		let y2 = norm w in
		let y3 = norm w' in
		let y4 = dist(w,w') in
		let y5 = dist(v,w') in
		let y6 = dist(v,w) in
		let y7 = norm u in
		let y8 = dist(w',u) in
		let y9 = dist(w,u) in
	tauVEF (V,E,face (hypermap_of_fan (V,E)) (v,w)) = tauq y1 y2 y3 y4 y5 y6 y7 y8 y9`
[
   ((BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card4"])))) THEN (repeat_tactic 11 0 ((CONV_TAC let_CONV))));
   ((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));
   ((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));
   ((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)));
   (((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] []))));
   ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
   ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E w' v`))) (term_tac (set_tac "w2")));
   ((fun arg_tac -> arg_tac (Arg_term (`_ INSERT E`))) (term_tac (set_tac "E2")));
   ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E2)`))) (term_tac (set_tac "H2")));
   (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"]));
   ((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"]))));
   (((((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));
   ((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)));
   ((((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("E2_def", []))(thm_tac (new_rewrite [] [])))));
   ((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)));
   ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E)`))) (term_tac (set_tac "H")));
   ((fun arg_tac -> arg_tac (Arg_term (`split_fan_face (V,E) (v,w) = (V,E2)`))) (term_tac (have_gen_tac [](move ["split_eq"]))));
   (((((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));
   ((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 [] [])))))));
   (((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))));
   ((((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));
   ((((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));
   (((((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));
   ((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 [] [])))))));
   (((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))));
   ((((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));
   ((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));
   ((((((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));
   (((((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));
];;

(* Finalization of the section EnclosedTauq *)
let taum_sym = Sections.finalize_theorem taum_sym;;
let fully_surrounded_enclosed = Sections.finalize_theorem fully_surrounded_enclosed;;
let fully_surrounded_tau_eq_tauq = Sections.finalize_theorem fully_surrounded_tau_eq_tauq;;
Sections.end_section "EnclosedTauq";;

(* Section Contravening *)
Sections.begin_section "Contravening";;
(Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
(Sections.add_section_hyp "contrV" (`contravening V`));;

(* Let fanV *)
Sections.add_section_lemma "fanV" (Sections.section_proof []
`FAN (vec 0,V,ESTD V)`
[
   (((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));
]);;

(* Let f_surr *)
Sections.add_section_lemma "f_surr" (Sections.section_proof []
`fully_surrounded (V,ESTD V)`
[
   (((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));
]);;

(* Let dart1_eq *)
Sections.add_section_lemma "dart1_eq" (Sections.section_proof []
`dart_of_fan (V,ESTD V) = dart1_of_fan (V,ESTD V)`
[
   (((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));
]);;

(* Lemma contravening_non_triangular_face_dist *)
let contravening_non_triangular_face_dist = Sections.section_proof ["v";"w"]
`v,w IN dart_of_fan (V,ESTD V)
	/\ 3 < CARD (face (hypermap_of_fan (V,ESTD V)) (v,w))
	==>	let w' = sigma_fan (vec 0) V (ESTD V) v w in
		let y1 = norm v in
		let y2 = norm w in
		let y3 = norm w' in
		let y4 = dist (w,w') in
		let y5 = dist (v,w') in
		let y6 = dist (v,w) in
			(&2 <= y1 /\ y1 <= &2 * h0) /\
			(&2 <= y2 /\ y2 <= &2 * h0) /\
			(&2 <= y3 /\ y3 <= &2 * h0) /\
			(&2 * h0 <= y4 /\ y4 <= &4 * h0) /\
			(&2 <= y5 /\ y5 <= &2 * h0) /\
			(&2 <= y6 /\ y6 <= &2 * h0)`
[
   ((BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card_gt3"])))) THEN (repeat_tactic 1 9 ((CONV_TAC let_CONV))));
   ((((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 [] []))))));
   ((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)));
   ((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"])));
   ((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"])));
   ((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"])));
   ((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"])));
   ((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"])))));
   ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _1 V _2 v w`))) (term_tac (set_tac "w'")));
   ((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 [] []))))));
   (((((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));
   ((((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 [] [])))))));
   ((((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));
   (((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));
   ((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)));
   (((((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));
];;

(* Section Ineqs *)
Sections.begin_section "Ineqs";;
(Sections.add_section_hyp "ineqs" (`kcblrqc_ineq_def`));;

(* Lemma non_triangular_face_azim_dart_bound *)
let non_triangular_face_azim_dart_bound = Sections.section_proof ["d"]
`d IN dart_of_fan (V,ESTD V)
	/\ 3 < CARD (face (hypermap_of_fan (V,ESTD V)) d)
	==> #1.15 < azim_dart (V,ESTD V) d`
[
   (((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"]))));
   ((((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 [] []))))));
   ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _1 V _2 v w`))) (term_tac (set_tac "w'")));
   (((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));
   ((((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));
   (((((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));
   ((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)));
   (((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));
   (((((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));
];;

(* Finalization of the section Ineqs *)
let non_triangular_face_azim_dart_bound = Sections.finalize_theorem non_triangular_face_azim_dart_bound;;
Sections.end_section "Ineqs";;

(* Finalization of the section Contravening *)
let contravening_non_triangular_face_dist = Sections.finalize_theorem contravening_non_triangular_face_dist;;
let non_triangular_face_azim_dart_bound = Sections.finalize_theorem non_triangular_face_azim_dart_bound;;
Sections.end_section "Contravening";;

(* Close the module *)
end;;