(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Appendix, Main Estimate, check_completeness                       *)
(* Chapter: Local Fan                                                         *)
(* Lemma: IUNBUIG                                                             *)
(* Author: Thomas Hales                                                       *)
(* Date: 2013-07-29                                                           *)
(* ========================================================================== *)

module Iunbuig = struct


open Hales_tactic;;


let LET_THM = CONJ LET_DEF LET_END_DEF;;


let quadratic_at_most_2_roots = 
prove_by_refinement(
  `!a b c. ?x1 x2. !x.
    ~(a = &0) /\ a * x pow 2 + b * x + c = &0 ==> x = x1 \/ x = x2`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  ASM_CASES_TAC `~(?x1. a * x1 pow 2 + b * x1 + c = &0)`;
    BY(ASM_MESON_TAC[]);
  FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC;
  ASM_CASES_TAC `!x2. a * x2 pow 2 + b * x2 + c = &0 ==> x2 = x1`;
    BY(ASM_MESON_TAC[]);
  FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM] THEN REPEAT STRIP_TAC;
  GEXISTL_TAC [`x1`;`x2`];
  BY(GEN_TAC THEN ASM_TAC THEN CONV_TAC REAL_RING)
(* String.length above = 414. String.length below = 233. 56% the length. *)
(*
g/r
asmcs `~(?x1. a * x1 pow 2 + b * x1 + c = &0)`
amt[]
fx mp then rt[] then str/r
asmcs `!x2. a * x2 pow 2 + b * x2 + c = &0 ==> x2 = x1` 
amt[]
fx mp then rt[NOT_FORALL_THM] then str/r
exl [`x1`;`x2`]
g then asm then cvc REAL_RING
*)
(*
If there are no roots, it is obvious. Otherwise, let x1 be a root.
If every root is x1 it is obvious. Otherwise, let x2 be a second root.
Instantiate the existential quantifiers with these two roots, and solve the resulting
problem by Groebner basis algorithm.
*)
]);;
  (* }}} *)

let ARCV_ADD_AFF_GE = 
prove_by_refinement(
  `!(u:real^N) v w x. ~(v = u) /\ ~(w = u) /\ ~(x = u) /\ x IN aff_ge {u} {v, w} ==>
    arcV u v x + arcV u x w = arcV u v w`,

  (* {{{ proof *)
  [
    BY(REWRITE_TAC[ARCV_ANGLE;ANGLES_ADD_AFF_GE])
  ]);;
  (* }}} *)

let SUM_NUMSEG4 = 
prove_by_refinement(
  `!t. sum (0..4) t = t 0 + t 1 + t 2 + t 3 + t 4`,

  (* {{{ proof *)
  [
  REWRITE_TAC[arith `4 = SUC 3`;SUM_CLAUSES_NUMSEG;Qknvmlb.SUM_NUMSEG3;arith `0 <= SUC 3`];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let epsilon_pent = 
prove_by_refinement(
  `!e e' e'' e''' e''''. &0 < e /\ &0 < e' /\ &0 < e'' /\ &0 < e''' /\ &0 < e'''' ==> (?e'''''. &0 < e''''' /\ (!t. abs t < e''''' ==> abs t < e) /\ (!t. abs t < e''''' ==> abs t < e') /\ (!t. abs t < e''''' ==> abs t < e'') /\ (!t. abs t < e''''' ==> abs t < e''') /\ (!t. abs t < e''''' ==> abs t < e''''))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Cuxvzoz.epsilon_quad [`e`;`e'`;`e''`;`e'''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Cuxvzoz.epsilon_pair [`e''''`;`e'''''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  TYPIFY `e''''''` EXISTS_TAC;
  BY(ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN (REPEAT (FIRST_X_ASSUM MATCH_MP_TAC)) THEN ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let epsilon_hex = 
prove_by_refinement(
  `!e e' e'' e''' e'''' e5. &0 < e /\ &0 < e' /\ &0 < e'' /\ &0 < e''' /\ &0 < e'''' /\ &0 < e5 ==> (?e6. &0 < e6 /\ (!t. abs t < e6 ==> abs t < e) /\ (!t. abs t < e6 ==> abs t < e') /\ (!t. abs t < e6 ==> abs t < e'') /\ (!t. abs t < e6 ==> abs t < e''') /\ (!t. abs t < e6 ==> abs t < e'''') /\ (!t. abs t < e6 ==> abs t < e5))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC epsilon_pent [`e`;`e'`;`e''`;`e'''`;`e''''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Cuxvzoz.epsilon_pair [`e'''''`;`e5`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  TYPIFY `e''''''` EXISTS_TAC;
  BY(ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN (REPEAT (FIRST_X_ASSUM MATCH_MP_TAC)) THEN ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let epsilon_hept = 
prove_by_refinement(
  `!e e' e'' e''' e'''' e5 e6. &0 < e /\ &0 < e' /\ &0 < e'' /\ &0 < e''' /\ &0 < e'''' /\ &0 < e5 /\ &0 < e6 ==> (?e7. &0 < e7 /\ (!t. abs t < e7 ==> abs t < e) /\ (!t. abs t < e7 ==> abs t < e') /\ (!t. abs t < e7 ==> abs t < e'') /\ (!t. abs t < e7 ==> abs t < e''') /\ (!t. abs t < e7 ==> abs t < e'''') /\ (!t. abs t < e7 ==> abs t < e5) /\ (!t. abs t < e7 ==> abs t < e6))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC epsilon_hex [`e`;`e'`;`e''`;`e'''`;`e''''`;`e5`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Cuxvzoz.epsilon_pair [`e6`;`e6'`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  TYPIFY `e'''''` EXISTS_TAC;
  BY(ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN (REPEAT (FIRST_X_ASSUM MATCH_MP_TAC)) THEN ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let re_eqvl_imp_le = 
prove_by_refinement(
  `!a b. re_eqvl a b ==> (&0 <= a <=> &0 <= b)`,

  (* {{{ proof *)
  [
  TYPIFY `!a b. re_eqvl a b /\ &0 <= b ==> &0 <= a` ENOUGH_TO_SHOW_TAC;
    BY(MESON_TAC[Leaf_cell.RE_EQVL_SYM]);
  REWRITE_TAC[Trigonometry2.re_eqvl];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC REAL_LE_MUL;
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let re_eqvl_real_sgn = 
prove_by_refinement(
  `!x y. re_eqvl x y <=> real_sgn x = real_sgn y`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC (TAUT `((a ==>b) /\ (b ==> a)) ==> (a = b)`);
  REWRITE_TAC[Trigonometry2.re_eqvl];
  CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[];
    REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[REAL_SGN_MUL;GSYM REAL_SGN_EQ;arith `&0 < t <=> t > &0`];
    BY(DISCH_THEN (unlist REWRITE_TAC) THEN REAL_ARITH_TAC);
  FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[REAL_SGN];
  TYPIFY `x = &0` ASM_CASES_TAC;
    ASM_REWRITE_TAC[arith `abs(&0) = &0`;arith `&0 / &0 = &0`;arith `&0 = x <=> x = &0`;REAL_DIV_EQ_0;REAL_ENTIRE;arith `abs y = &0 <=> y = &0`];
    BY(MESON_TAC[arith `&0 < &1`]);
  DISCH_TAC;
  TYPIFY `~(y = &0)` (C SUBGOAL_THEN ASSUME_TAC);
    DISCH_TAC;
    FIRST_X_ASSUM_ST `abs` MP_TAC;
    BY(ASM_REWRITE_TAC[arith `&0 / t = &0`;REAL_DIV_EQ_0] THEN ASM_TAC THEN REAL_ARITH_TAC);
  TYPIFY `x / y` EXISTS_TAC;
  CONJ2_TAC;
    Calc_derivative.CALC_ID_TAC;
    BY(ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
  REWRITE_TAC[Calc_derivative.invert_den_lt];
  REWRITE_TAC[REAL_MUL_POS_LT];
  FIRST_X_ASSUM_ST `abs` MP_TAC THEN REWRITE_TAC[GSYM REAL_SGN;real_sgn];
  RULE_ASSUM_TAC (REWRITE_RULE[arith `~(x = &0) <=> (&0 < x \/ x < &0) /\ ~(&0 < x /\ x < &0)`]);
  ASSUME_TAC (arith ` ~(&1 = -- &1)`);
  BY(REPEAT COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let coplanar_delta_y_zero = 
prove_by_refinement(
  `!(u0:real^3) u1 u2 u3. coplanar  {u0, u1, u2, u3} <=>
            delta_y (dist (u0,u1)) (dist (u0,u2)) (dist (u0,u3))
            (dist (u2,u3))
            (dist (u1,u3))
            (dist (u1,u2)) = &0`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_MESON_TAC[Terminal.DELTA_Y_POS_4POINTS;Oxlzlez.coplanar_delta_y;arith `&0 <= x ==> (~(&0 < x) <=> (x = &0))`])
  ]);;
  (* }}} *)

let real_continuous_finite_range_constant = 
prove_by_refinement(
  `!f a b. f real_continuous_on (real_interval (a,b)) /\ FINITE (IMAGE f (real_interval (a,b))) ==>
    (?c. !x. x IN real_interval (a,b) ==> f x = c)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `(?c. !x. x IN IMAGE lift (real_interval(a,b)) ==> ((lift o f o drop) x = c))` ENOUGH_TO_SHOW_TAC;
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `drop c` EXISTS_TAC;
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM_ST `IMAGE` (C INTRO_TAC [`lift x`]);
    REWRITE_TAC[o_THM;LIFT_DROP];
    ANTS_TAC;
      MATCH_MP_TAC FUN_IN_IMAGE;
      BY(ASM_REWRITE_TAC[]);
    DISCH_THEN (SUBST1_TAC o GSYM);
    BY(REWRITE_TAC[LIFT_DROP]);
  MATCH_MP_TAC CONTINUOUS_FINITE_RANGE_CONSTANT;
  CONJ_TAC;
    ONCE_REWRITE_TAC[GSYM LIFT_DROP];
    REWRITE_TAC[GSYM INTERVAL_REAL_INTERVAL];
    BY(REWRITE_TAC[CONNECTED_INTERVAL]);
  CONJ_TAC;
    REWRITE_TAC[ETA_AX];
    BY(ASM_REWRITE_TAC[GSYM REAL_CONTINUOUS_ON]);
  REWRITE_TAC[GSYM IMAGE_o;ETA_AX;GSYM o_ASSOC];
  TYPIFY_GOAL_THEN `!X. IMAGE (lift o f o drop o lift) X = IMAGE lift (IMAGE f (IMAGE (drop o lift) X))` (unlist REWRITE_TAC);
    BY(REWRITE_TAC[GSYM IMAGE_o;GSYM o_ASSOC]);
  REWRITE_TAC[IMAGE_LIFT_DROP];
  MATCH_MP_TAC FINITE_IMAGE;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let planar_deform_dist = 
prove_by_refinement(
  `!(v0:real^3) v1 v2 f V e'.
    v1 IN V /\ v2 IN V /\ ~(v0 = vec 0) /\
    &0 < e' /\ deformation f V (--e',e') /\ (!v t. ~(v  =v1) /\ ~(v = v2) ==> f v t = v) /\
(!t. abs t < e'
                 ==> coplanar {vec 0, v0, f v1 t, f v2 t} /\
                     dist (v0,f v1 t) = dist (v0,v1) /\
                     norm (f v1 t) = norm v1 /\
                     dist (f v2 t,v0) = dist (v2,v0) /\
                     norm (f v2 t) = norm v2) ==>
    (!t. abs t < e' ==> dist(f v1 t,f v2 t) = dist(v1,v2))
`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `f v1 (&0) = v1 /\ f v2 (&0) = v2` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
    BY(ASM_MESON_TAC[]);
  TYPED_ABBREV_TAC `b = ((norm v0 * norm v0) * norm v0 * norm v0 +      (norm v2 * norm v2 - dist (v0,v2) * dist (v0,v2)) *      (norm v1 * norm v1 - dist (v0,v1) * dist (v0,v1)) -      (norm v0 * norm v0) *      (norm v1 * norm v1 +       norm v2 * norm v2 +       dist (v0,v2) * dist (v0,v2) +       dist (v0,v1) * dist (v0,v1)))`;
  TYPED_ABBREV_TAC `c = (norm v0 * norm v0) * (norm v2 * norm v2) * dist (v0,v2) * dist (v0,v2) +     (norm v0 * norm v0) * (norm v1 * norm v1) * dist (v0,v1) * dist (v0,v1) -     (norm v2 * norm v2) *     (norm v0 * norm v0 +      norm v1 * norm v1 - norm v2 * norm v2 +      dist (v0,v2) * dist (v0,v2) - dist (v0,v1) * dist (v0,v1)) *     dist (v0,v1) *     dist (v0,v1) -     (norm v1 * norm v1) *     (dist (v0,v2) * dist (v0,v2)) *     (norm v0 * norm v0 - norm v1 * norm v1 +      norm v2 * norm v2 - dist (v0,v2) * dist (v0,v2) +      dist (v0,v1) * dist (v0,v1))`;
  TYPED_ABBREV_TAC `a = (norm v0 * norm v0)`;
  INTRO_TAC quadratic_at_most_2_roots [`a`;`b`;`c`];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC real_continuous_finite_range_constant [`(\t. dist(f v1 t, f v2 t))`;`-- e'`;`e'`];
  ANTS_TAC;
    CONJ_TAC;
      GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
      REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
      REPEAT WEAKER_STRIP_TAC;
      MATCH_MP_TAC Local_lemmas1.CON_ATREAL_REAL_CON2_REDO;
      FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation;ETA_AX];
      BY(ASM_MESON_TAC[]);
    TYPIFY `IMAGE (\t. dist (f v1 t,f v2 t) pow 2) (real_interval (--e',e')) SUBSET {x1,x2}` ENOUGH_TO_SHOW_TAC;
      TYPIFY `FINITE {x1,x2}` ENOUGH_TO_SHOW_TAC;
        TYPIFY_GOAL_THEN `!X. IMAGE (\t. dist (f v1 t,f v2 t) pow 2) X = IMAGE (\t. t pow 2) (IMAGE (\t. dist (f v1 t,f v2 t)) X)` (unlist REWRITE_TAC);
          REWRITE_TAC[GSYM IMAGE_o];
          BY(GEN_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM;o_THM]);
        TYPED_ABBREV_TAC `s = (IMAGE (\t. dist (f v1 t,f v2 t)) (real_interval (--e',e')))`;
        INTRO_TAC HAS_SIZE_IMAGE_INJ_EQ [`(\t. t pow 2)`;`s`;`CARD (IMAGE (\t. t pow 2) s)`];
        ANTS_TAC;
          EXPAND_TAC "s";
          REWRITE_TAC[IN_IMAGE] THEN REPEAT WEAKER_STRIP_TAC;
          FIRST_X_ASSUM MP_TAC;
          ASM_REWRITE_TAC[];
          REWRITE_TAC[GSYM REAL_EQ_SQUARE_ABS];
          REPEAT (GMATCH_SIMP_TAC (arith `&0 <= x ==> abs x = x`));
          BY(REWRITE_TAC[DIST_POS_LE]);
        REWRITE_TAC[HAS_SIZE];
        BY(MESON_TAC[FINITE_SUBSET;FINITE_IMAGE]);
      BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
    REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_IMAGE];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    CONJ_TAC;
      EXPAND_TAC "a";
      REWRITE_TAC[REAL_ENTIRE];
      REWRITE_TAC[NORM_EQ_0];
      BY(ASM_REWRITE_TAC[]);
    FIRST_X_ASSUM_ST `coplanar` (C INTRO_TAC [`x'`]);
    ANTS_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[IN_REAL_INTERVAL;arith `-- e < t /\ t < e <=> abs t < e`]);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM_ST `coplanar` MP_TAC THEN REWRITE_TAC[coplanar_delta_y_zero];
    REPEAT (FIRST_X_ASSUM_ST `dist` MP_TAC) THEN REWRITE_TAC[DIST_SYM;DIST_0] THEN REPEAT WEAKER_STRIP_TAC THEN (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[];
    ONCE_REWRITE_TAC[arith `x = &0 <=> -- x = &0`];
    ASM_REWRITE_TAC[Sphere.delta_y;Nonlinear_lemma.delta_quadratic];
    BY(REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  FIRST_ASSUM (C INTRO_TAC [`&0`]);
  FIRST_X_ASSUM (C INTRO_TAC [`t`]);
  REWRITE_TAC[];
  REPEAT (DISCH_THEN GMATCH_SIMP_TAC);
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM_ST `deformation` MP_TAC THEN ASM_REWRITE_TAC[Localization.deformation;IN_REAL_INTERVAL;arith `--e < t /\ t < e <=> abs t < e`;arith `abs(&0) = &0`];
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

(*
let deform_pent_exists = prove_by_refinement(
  `!V g23 v0 v1 v2 v3 e. ?f.
    (
       (    v1 IN V /\ v2 IN V /\ 
	      (coplanar {vec 0,v0,v1,v2} ==> (v1 cross v0) dot (v2 cross v0) > &0) /\
			~coplanar {vec 0,v0,v2,v3} /\ ~(collinear {vec 0,v1,v2}) /\
	  &0 < azim (vec 0) v1 v2 v0 /\ azim (vec 0) v1 v2 v0 <= pi /\
	  v2 dot (v3 cross v0) > &0 /\ 
	  &0 < e /\
	  g23 real_continuous_on (real_interval (--e,e)) /\
	  g23 (&0) = &0 
	==> 
	  (?e'. &0 < e' /\ deformation f V (-- e', e') /\
	     (!v t. ~(v = v1) /\ ~(v = v2) ==> f v t = v) /\
	     (!t. abs t < e' ==> 
		dist(v0,f v1 t) = dist(v0,v1) /\
		dist(f v2 t,f v1 t) = dist(v2,v1) /\
		norm(f v1 t) = norm(v1) /\
		  dist (f v2 t,v0) = dist(v2,v0) /\
		  dist (f v2 t,v3) = dist(v2,v3)+ g23 t /\
		  norm(f v2 t) = norm (v2)
	     ))))`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[MESON [] `(?f. a ==> P f) <=> (a ==> (?f. P f))`];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~coplanar {vec 0,v0,v1,v2}` ASM_CASES_TAC;
    INTRO_TAC Cuxvzoz.deform_684_pent_exists [`V`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[];
    REWRITE_TAC[arith `x > &0 <=> &0 <= x /\ ~(x = &0)`];
    ANTS_TAC;
      ASM_REWRITE_TAC[];
      CONJ2_TAC;
        BY(REPEAT (FIRST_X_ASSUM_ST `coplanar` MP_TAC) THEN REWRITE_TAC[GSYM Local_lemmas.CROSS_DOT_COPLANAR] THEN VEC3_TAC);
      INTRO_TAC Trigonometry2.JBDNJJB [`v1`;`v2`;`v0`];
      TYPIFY `((v1 cross v2) dot v0) = v1 dot (v2 cross v0)` (C SUBGOAL_THEN SUBST1_TAC);
        BY(VEC3_TAC);
      ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
      DISCH_THEN ((unlist REWRITE_TAC) o (MATCH_MP re_eqvl_imp_le));
      BY(ASM_MESON_TAC[Local_lemmas.SIN_AZIM_POS_PI_LT]);
    REPEAT WEAKER_STRIP_TAC;
    BY(GEXISTL_TAC [`f`;`e'`] THEN ASM_MESON_TAC[]);
  COMMENT "planar case";
  INTRO_TAC Cuxvzoz.deform_planar_exists [`V`;`(\ (t:real). &0)`;`(\ (t:real). &0)`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
  RULE_ASSUM_TAC(REWRITE_RULE[]);
  REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[arith `x + &0 = x`];
  GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;Ocbicby.REAL_OPEN_REAL_INTERVAL];
  ANTS_TAC;
    CONJ_TAC;
      BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
    BY(FIRST_X_ASSUM_ST `collinear` MP_TAC THEN MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b} = {a,b}`]);
  REPEAT WEAKER_STRIP_TAC;
  GEXISTL_TAC [`f`;`e'`] THEN ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~(v0 = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[COPLANAR_3;SET_RULE `{a,a,b,c} = {a,b,c}`]);
  INTRO_TAC planar_deform_dist [`v0`;`v1`;`v2`;`f`;`V`;`e'`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    BY(ASM_MESON_TAC[]);
  DISCH_TAC;
  BY(REPLICATE_TAC 2 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[DIST_SYM] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)
*)

(*
let deform_pent_exists = prove_by_refinement(
  `!V g23 v0 v1 v2 v3 e. ?f.
    (
       (    v1 IN V /\ v2 IN V /\ 
	      (coplanar {vec 0,v0,v1,v2} ==> (v1 cross v0) dot (v2 cross v0) > &0) /\
			~coplanar {vec 0,v0,v2,v3} /\ ~(collinear {vec 0,v1,v2}) /\
	      azim (vec 0) v1 v2 v0 <= pi /\
	  v2 dot (v3 cross v0) > &0 /\ 
	  &0 < e /\
	  g23 real_continuous_on (real_interval (--e,e)) /\
	  g23 (&0) = &0 
	==> 
	  (?e'. &0 < e' /\ deformation f V (-- e', e') /\
	     (!v t. ~(v = v1) /\ ~(v = v2) ==> f v t = v) /\
	     (!t. abs t < e' ==> 
		dist(v0,f v1 t) = dist(v0,v1) /\
		dist(f v2 t,f v1 t) = dist(v2,v1) /\
		norm(f v1 t) = norm(v1) /\
		  dist (f v2 t,v0) = dist(v2,v0) /\
		  dist (f v2 t,v3) = dist(v2,v3)+ g23 t /\
		  norm(f v2 t) = norm (v2)
	     ))))`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[MESON [] `(?f. a ==> P f) <=> (a ==> (?f. P f))`];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~coplanar {vec 0,v0,v1,v2}` ASM_CASES_TAC;
    INTRO_TAC Cuxvzoz.deform_684_pent_exists [`V`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[];
    REWRITE_TAC[arith `x > &0 <=> &0 <= x /\ ~(x = &0)`];
    ANTS_TAC;
      ASM_REWRITE_TAC[];
      CONJ2_TAC;
        BY(REPEAT (FIRST_X_ASSUM_ST `coplanar` MP_TAC) THEN REWRITE_TAC[GSYM Local_lemmas.CROSS_DOT_COPLANAR] THEN VEC3_TAC);
      INTRO_TAC Trigonometry2.JBDNJJB [`v1`;`v2`;`v0`];
      TYPIFY `((v1 cross v2) dot v0) = v1 dot (v2 cross v0)` (C SUBGOAL_THEN SUBST1_TAC);
        BY(VEC3_TAC);
      ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
      DISCH_THEN ((unlist REWRITE_TAC) o (MATCH_MP re_eqvl_imp_le));
      BY(ASM_MESON_TAC[Local_lemmas.SIN_AZIM_POS_PI_LT]);
    REPEAT WEAKER_STRIP_TAC;
    BY(GEXISTL_TAC [`f`;`e'`] THEN ASM_MESON_TAC[]);
  COMMENT "planar case";
  INTRO_TAC Cuxvzoz.deform_planar_exists [`V`;`(\ (t:real). &0)`;`(\ (t:real). &0)`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
  RULE_ASSUM_TAC(REWRITE_RULE[]);
  REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[arith `x + &0 = x`];
  GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;Ocbicby.REAL_OPEN_REAL_INTERVAL];
  ANTS_TAC;
    CONJ_TAC;
      BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
    BY(FIRST_X_ASSUM_ST `collinear` MP_TAC THEN MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b} = {a,b}`]);
  REPEAT WEAKER_STRIP_TAC;
  GEXISTL_TAC [`f`;`e'`] THEN ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~(v0 = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[COPLANAR_3;SET_RULE `{a,a,b,c} = {a,b,c}`]);
  INTRO_TAC planar_deform_dist [`v0`;`v1`;`v2`;`f`;`V`;`e'`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    BY(ASM_MESON_TAC[]);
  DISCH_TAC;
  BY(REPLICATE_TAC 2 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[DIST_SYM] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)
*)

let deform_pent_exists = 
prove_by_refinement(
  `!V g23 v0 v1 v2 v3 e. ?f.
           v1 IN V /\ v2 IN V /\ 
	      (coplanar {vec 0,v0,v1,v2} ==> (v1 cross v0) dot (v2 cross v0) > &0) /\
			~coplanar {vec 0,v0,v2,v3} /\ ~(collinear {vec 0,v1,v2}) /\
	      azim (vec 0) v1 v2 v0 <= pi /\
	  v2 dot (v3 cross v0) > &0 /\ 
	  &0 < e /\
	  g23 real_continuous_on (real_interval (--e,e)) /\
	  g23 (&0) = &0 
	==> 
	  (?e'. &0 < e' /\ deformation f V (-- e', e') /\
	     (!v t. ~(v = v1) /\ ~(v = v2) ==> f v t = v) /\
	     (!t. abs t < e' ==> 
		dist(v0,f v1 t) = dist(v0,v1) /\
		dist(f v2 t,f v1 t) = dist(v2,v1) /\
		norm(f v1 t) = norm(v1) /\
		  dist (f v2 t,v0) = dist(v2,v0) /\
		  dist (f v2 t,v3) = dist(v2,v3)+ g23 t /\
		  norm(f v2 t) = norm (v2) /\
		  (coplanar {vec 0,v0,v1,v2} ==> coplanar {vec 0,v0,f v1 t,f v2 t})
	     ))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[MESON [] `(?f. a ==> P f) <=> (a ==> (?f. P f))`];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~coplanar {vec 0,v0,v1,v2}` ASM_CASES_TAC;
    INTRO_TAC Cuxvzoz.deform_684_pent_exists [`V`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[];
    REWRITE_TAC[arith `x > &0 <=> &0 <= x /\ ~(x = &0)`];
    ANTS_TAC;
      ASM_REWRITE_TAC[];
      CONJ2_TAC;
        BY(REPEAT (FIRST_X_ASSUM_ST `coplanar` MP_TAC) THEN REWRITE_TAC[GSYM Local_lemmas.CROSS_DOT_COPLANAR] THEN VEC3_TAC);
      INTRO_TAC Trigonometry2.JBDNJJB [`v1`;`v2`;`v0`];
      TYPIFY `((v1 cross v2) dot v0) = v1 dot (v2 cross v0)` (C SUBGOAL_THEN SUBST1_TAC);
        BY(VEC3_TAC);
      ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
      DISCH_THEN ((unlist REWRITE_TAC) o (MATCH_MP re_eqvl_imp_le));
      BY(ASM_MESON_TAC[Local_lemmas.SIN_AZIM_POS_PI_LT]);
    REPEAT WEAKER_STRIP_TAC;
    BY(GEXISTL_TAC [`f`;`e'`] THEN ASM_MESON_TAC[]);
  COMMENT "planar case";
  INTRO_TAC Cuxvzoz.deform_planar_exists [`V`;`(\ (t:real). &0)`;`(\ (t:real). &0)`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
  RULE_ASSUM_TAC(REWRITE_RULE[]);
  REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[arith `x + &0 = x`];
  GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;Ocbicby.REAL_OPEN_REAL_INTERVAL];
  ANTS_TAC;
    CONJ_TAC;
      BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
    BY(FIRST_X_ASSUM_ST `collinear` MP_TAC THEN MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b} = {a,b}`]);
  REPEAT WEAKER_STRIP_TAC;
  GEXISTL_TAC [`f`;`e'`] THEN ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~(v0 = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[COPLANAR_3;SET_RULE `{a,a,b,c} = {a,b,c}`]);
  INTRO_TAC planar_deform_dist [`v0`;`v1`;`v2`;`f`;`V`;`e'`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    BY(ASM_MESON_TAC[]);
  DISCH_TAC;
  BY(REPLICATE_TAC 2 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[DIST_SYM] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

(*
let EGHNAVX_SCS = prove_by_refinement(
  `!s k v p.  
    (let bta = (\j.  azim (vec 0) (v p) (v (p+1)) (v (p+j))) in 
    (    is_scs_v39 s /\ scs_k_v39 s = k /\
	3 < k /\ 
         BBs_v39 s v /\
	scs_basic_v39 s /\ 
	 scs_generic v ==>
	   bta 1 = &0 /\
            bta (k - 1) <= pi /\
            (!i j. i < j /\ j < k ==> bta i <= bta j) /\
            (!q j. bta q = &0 /\ 0 < j /\ j <= q /\ q < k 
                      ==> (j<q ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v (p+j+k-1)) = pi) /\
                  v (p+j) IN aff_gt {vec 0,v p} {v (p+1)}) /\ 
            (!q j. bta q = bta (k - 1) /\ 0 < q /\ q < k - 1 /\ q <= j /\ j < k
                      ==> (q < j ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v(p+j+k-1)) = pi) /\
		  v(p+j) IN aff_gt {vec 0, v p} {v (p + k - 1)})))`,
  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  LET_TAC;
  REPEAT WEAKER_STRIP_TAC;
  TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
  TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
  TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
  INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`k`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `periodic v k /\ convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN ASM_MESON_TAC[arith `3 < k ==> ~(k<= 3)`]);
  INTRO_TAC Terminal.ITER_vv_rho_node1 [`v`;`k`];
  ASM_REWRITE_TAC[LET_THM];
  TYPIFY_GOAL_THEN `3 <= k` (unlist REWRITE_TAC);
    BY(ASM_MESON_TAC[arith `3 < k ==> 3 <= k`]);
  DISCH_TAC;
  INTRO_TAC (GEN_ALL Odxlstcv2.CARD_V_EQ_SCS_K1) [`s`;`v`;`V`;`k`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    EXPAND_TAC "V";
    MATCH_MP_TAC FUN_IN_IMAGE;
    BY(REWRITE_TAC[IN_UNIV]);
  TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0, v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN [`V`;`E`;`FF`];
    BY(ASM_MESON_TAC[Appendix.scs_generic]);
  INTRO_TAC (GENL [`v0:real^3`;`vv:num->real^3`;`i:num`] Local_lemmas.EGHNAVX) [`v p`;`\ (i:num). v (p + i)`];
  REWRITE_TAC[RIGHT_FORALL_IMP_THM;GSYM RIGHT_AND_FORALL_THM];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      TYPIFY `?i'. v' = v i'` (C SUBGOAL_THEN MP_TAC);
        FIRST_X_ASSUM_ST `IN` MP_TAC;
        EXPAND_TAC "V";
        BY(REWRITE_TAC[IN_IMAGE;IN_UNIV]);
      REPEAT WEAKER_STRIP_TAC;
      BY(ASM_MESON_TAC[]);
    EXPAND_TAC "bta";
    BY(REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  INTRO_TAC (GSYM Ocbicby.INTERIOR_ANGLE1_AZIM) [`s`;`v`];
  ASM_REWRITE_TAC[LET_THM];
  TYPIFY_GOAL_THEN `v IN BBs_v39 s` (unlist REWRITE_TAC);
    BY(ASM_REWRITE_TAC[IN]);
  DISCH_TAC;
  COMMENT "first conjunct";
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM_ST `SUBSET` (C INTRO_TAC [`q`]);
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    CONJ_TAC;
      DISCH_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`j`]);
      ASM_REWRITE_TAC[];
      BY(REWRITE_TAC[arith `SUC (p+j) = p+j+1 /\ ((p+j) + k - 1 = p+j+k-1)`]);
    FIRST_X_ASSUM kill;
    FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM];
    DISCH_THEN (C INTRO_TAC [`v (p+(j:num))`]);
    DISCH_THEN MATCH_MP_TAC;
    BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `SUBSET` (C INTRO_TAC [`q`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  CONJ_TAC;
    DISCH_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`j`]);
    ASM_REWRITE_TAC[];
    BY(REWRITE_TAC[arith `SUC (p+j) = p+j+1 /\ ((p+j) + k - 1 = p+j+k-1)`]);
  FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM];
  DISCH_THEN (C INTRO_TAC [`v (p+(j:num))`]);
  DISCH_THEN MATCH_MP_TAC;
  BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[])
  ]);;
  (* }}} *)
*)

let EGHNAVX_COLL_SCS = 
prove_by_refinement(
  `!s k v p.  
    (let bta = (\j.  azim (vec 0) (v p) (v (p+1)) (v (p+j))) in 
    (    is_scs_v39 s /\ scs_k_v39 s = k /\
	3 < k /\ 
         BBs_v39 s v /\
	scs_basic_v39 s /\ 
	(!i. ~(v i = v p) ==> ~collinear {vec 0,v p,v i})
	==>
	   bta 1 = &0 /\
            bta (k - 1) <= pi /\
            (!i j. i < j /\ j < k ==> bta i <= bta j) /\
            (!q j. bta q = &0 /\ 0 < j /\ j <= q /\ q < k 
                      ==> (j<q ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v (p+j+k-1)) = pi) /\
                  v (p+j) IN aff_gt {vec 0,v p} {v (p+1)}) /\ 
            (!q j. bta q = bta (k - 1) /\ 0 < q /\ q < k - 1 /\ q <= j /\ j < k
                      ==> (q < j ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v(p+j+k-1)) = pi) /\
		  v(p+j) IN aff_gt {vec 0, v p} {v (p + k - 1)})))`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  LET_TAC;
  REPEAT WEAKER_STRIP_TAC;
  TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
  TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
  TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
  INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`k`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `periodic v k /\ convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN ASM_MESON_TAC[arith `3 < k ==> ~(k<= 3)`]);
  INTRO_TAC Terminal.ITER_vv_rho_node1 [`v`;`k`];
  ASM_REWRITE_TAC[LET_THM];
  TYPIFY_GOAL_THEN `3 <= k` (unlist REWRITE_TAC);
    BY(ASM_MESON_TAC[arith `3 < k ==> 3 <= k`]);
  DISCH_TAC;
  INTRO_TAC (GEN_ALL Odxlstcv2.CARD_V_EQ_SCS_K1) [`s`;`v`;`V`;`k`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    EXPAND_TAC "V";
    MATCH_MP_TAC FUN_IN_IMAGE;
    BY(REWRITE_TAC[IN_UNIV]);
  INTRO_TAC (GENL [`v0:real^3`;`vv:num->real^3`;`i:num`] Local_lemmas.EGHNAVX) [`v p`;`\ (i:num). v (p + i)`];
  REWRITE_TAC[RIGHT_FORALL_IMP_THM;GSYM RIGHT_AND_FORALL_THM];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    CONJ_TAC;
      EXPAND_TAC "V";
      (REWRITE_TAC[IN_IMAGE;IN_UNIV]);
      BY(ASM_MESON_TAC[]);
    EXPAND_TAC "bta";
    BY(REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  INTRO_TAC (GSYM Ocbicby.INTERIOR_ANGLE1_AZIM) [`s`;`v`];
  ASM_REWRITE_TAC[LET_THM];
  TYPIFY_GOAL_THEN `v IN BBs_v39 s` (unlist REWRITE_TAC);
    BY(ASM_REWRITE_TAC[IN]);
  DISCH_TAC;
  COMMENT "first conjunct";
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM_ST `SUBSET` (C INTRO_TAC [`q`]);
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    CONJ_TAC;
      DISCH_TAC;
      FIRST_X_ASSUM (C INTRO_TAC [`j`]);
      ASM_REWRITE_TAC[];
      BY(REWRITE_TAC[arith `SUC (p+j) = p+j+1 /\ ((p+j) + k - 1 = p+j+k-1)`]);
    FIRST_X_ASSUM kill;
    FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM];
    DISCH_THEN (C INTRO_TAC [`v (p+(j:num))`]);
    DISCH_THEN MATCH_MP_TAC;
    BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `SUBSET` (C INTRO_TAC [`q`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  CONJ_TAC;
    DISCH_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`j`]);
    ASM_REWRITE_TAC[];
    BY(REWRITE_TAC[arith `SUC (p+j) = p+j+1 /\ ((p+j) + k - 1 = p+j+k-1)`]);
  FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM];
  DISCH_THEN (C INTRO_TAC [`v (p+(j:num))`]);
  DISCH_THEN MATCH_MP_TAC;
  BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[])
  ]);;
  (* }}} *)

let EGHNAVX_SCS = 
prove_by_refinement(
  `!s k v p.  
    (let bta = (\j.  azim (vec 0) (v p) (v (p+1)) (v (p+j))) in 
    (    is_scs_v39 s /\ scs_k_v39 s = k /\
	3 < k /\ 
         BBs_v39 s v /\
	scs_basic_v39 s /\ 
	 scs_generic v ==>
	   bta 1 = &0 /\
            bta (k - 1) <= pi /\
            (!i j. i < j /\ j < k ==> bta i <= bta j) /\
            (!q j. bta q = &0 /\ 0 < j /\ j <= q /\ q < k 
                      ==> (j<q ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v (p+j+k-1)) = pi) /\
                  v (p+j) IN aff_gt {vec 0,v p} {v (p+1)}) /\ 
            (!q j. bta q = bta (k - 1) /\ 0 < q /\ q < k - 1 /\ q <= j /\ j < k
                      ==> (q < j ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v(p+j+k-1)) = pi) /\
		  v(p+j) IN aff_gt {vec 0, v p} {v (p + k - 1)})))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[LET_THM];
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC (REWRITE_RULE[LET_THM] EGHNAVX_COLL_SCS);
  TYPIFY `s` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `scs_generic` MP_TAC;
  REWRITE_TAC[Appendix.scs_generic];
  DISCH_TAC;
  TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
  TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
  TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
  TYPIFY `convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN ASM_MESON_TAC[arith `3 < k ==> ~(k<= 3)`]);
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    EXPAND_TAC "V";
    MATCH_MP_TAC FUN_IN_IMAGE;
    BY(REWRITE_TAC[IN_UNIV]);
  BY(ASM_MESON_TAC[Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN])
  ]);;
  (* }}} *)

let coplanar_cross_reduction = 
prove_by_refinement(
  `!s k v i.
    is_scs_v39 s /\ scs_k_v39 s = k /\
      3 < k /\ 
         MMs_v39 s v /\
      scs_basic_v39 s /\ 
	 scs_generic v /\ 
	 coplanar {vec 0,v i, v(i+1),v(i+2)} ==>
	 (v(i+1) cross v i) dot (v(i+2) cross v i) > &0`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~(k=0)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
  TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
  TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
  FIRST_ASSUM_ST `coplanar` MP_TAC;
  REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
  DISCH_TAC;
  TYPIFY `~coplanar ({vec 0} UNION V)` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "V";
    MATCH_MP_TAC Fektyiy.FEKTYIY;
    TYPIFY `s` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[IN]);
  TYPIFY `BBprime2_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Appendix.scs_basic;Ayqjtmd.unadorned_MMs]);
  TYPIFY `BBprime_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Appendix.BBprime2_v39]);
  TYPIFY `BBs_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Appendix.BBprime_v39]);
  INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`k`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `periodic v k /\ convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN ASM_MESON_TAC[arith `3 < k ==> ~(k<= 3)`]);
  INTRO_TAC Terminal.ITER_vv_rho_node1 [`v`;`k`];
  ASM_REWRITE_TAC[LET_THM];
  ASM_SIMP_TAC[arith `3 < k ==> 3 <= k`];
  DISCH_TAC;
  INTRO_TAC (GEN_ALL Odxlstcv2.CARD_V_EQ_SCS_K1) [`s`;`v`;`V`;`k`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    EXPAND_TAC "V";
    MATCH_MP_TAC FUN_IN_IMAGE;
    BY(REWRITE_TAC[IN_UNIV]);
  TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0, v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
    INTRO_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN [`V`;`E`;`FF`];
    BY(ASM_MESON_TAC[Appendix.scs_generic]);
  INTRO_TAC EGHNAVX_SCS [`s`;`k`;`v`;`i`];
  REWRITE_TAC[LET_THM];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "insert here";
  TYPIFY `!a. 0 < a /\ (a:num) < k ==> ~(v i = v (i+a))` (C SUBGOAL_THEN ASSUME_TAC);
    TYPIFY `!i. v (i MOD k) = v i` (C SUBGOAL_THEN ASSUME_TAC);
      GEN_TAC;
      MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
      BY(ASM_MESON_TAC[arith `3 < k ==> ~(0=k)`]);
    FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
    GEN_TAC THEN DISCH_TAC;
    TYPIFY_GOAL_THEN `!i j. i < k /\ j < (k:num) /\ ~(i = j) ==> ~(v i = v j)` MATCH_MP_TAC;
      BY(ASM_MESON_TAC[]);
    REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC;
      BY(ASM_MESON_TAC[DIVISION]);
    TYPIFY `i MOD k = (i+0) MOD k` (C SUBGOAL_THEN SUBST1_TAC);
      BY(REWRITE_TAC[arith `i + 0 = i`]);
    GMATCH_SIMP_TAC Ocbicby.MOD_EQ_MOD_SHIFT;
    REPEAT (GMATCH_SIMP_TAC MOD_LT);
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
  FIRST_X_ASSUM DISJ_CASES_TAC;
    FIRST_X_ASSUM_ST `&0` (C INTRO_TAC [`2`;`2`]);
    ASM_REWRITE_TAC[arith `0 < 2 /\ 2 <= 2 /\ ~(2 < 2)`];
    ANTS_TAC;
      BY(MATCH_MP_TAC (arith `3 < k ==> 2 < k`) THEN ASM_REWRITE_TAC[]);
    GMATCH_SIMP_TAC Local_lemmas1.COLL_AFF_GT_2_1;
    SUBCONJ_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
    DISCH_TAC;
    REWRITE_TAC[IN_ELIM_THM];
    REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[CROSS_LMUL;CROSS_LADD;DOT_RMUL;DOT_RADD;CROSS_LZERO;DOT_RZERO;CROSS_REFL];
    REWRITE_TAC[arith `t1 * &0 + x = x`;arith `x > &0 <=> &0 < x`];
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[DOT_POS_LT];
    REWRITE_TAC[CROSS_EQ_0];
    ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
    BY(ASM_REWRITE_TAC[]);
  COMMENT "second conj";
  FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`2`]);
  FIRST_X_ASSUM_ST `aff_gt` kill;
  FIRST_X_ASSUM_ST `0 < a` MP_TAC THEN BURY_MP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`2`;`k-1`]);
  ANTS_TAC;
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  DISCH_TAC;
  TYPIFY_GOAL_THEN `azim (vec 0) (v i) (v (i + 1)) (v (i + 2)) =      azim (vec 0) (v i) (v (i + 1)) (v (i + k - 1))` (unlist REWRITE_TAC);
    BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  DISCH_TAC;
  PROOF_BY_CONTR_TAC;
  TYPIFY `V SUBSET affine hull {vec 0,v i,v (i+k-1)}` ENOUGH_TO_SHOW_TAC;
    DISCH_TAC THEN FIRST_X_ASSUM_ST `coplanar` MP_TAC THEN REWRITE_TAC[coplanar];
    GEXISTL_TAC [`(vec 0):real^3`;`v i`;`v (i+k-1)`];
    FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_UNION;IN_SING];
    TYPIFY `vec 0 IN affine hull {vec 0,v i ,v(i+k-1)}` ENOUGH_TO_SHOW_TAC;
      BY(MESON_TAC[]);
    MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
    BY(SET_TAC[]);
  TYPIFY `!w. w IN IMAGE v (i..i + k - 1) ==> w IN affine hull {vec 0,v i , v(i+k-1)}` ENOUGH_TO_SHOW_TAC;
    GMATCH_SIMP_TAC (GSYM Oxl_2012.PERIODIC_IMAGE_EQUAL);
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    INTRO_TAC Oxl_def.periodic_numseg [`(\j. v j IN affine hull {vec 0,v i,v (i+k-1)})`;`k`];
    ASM_REWRITE_TAC[];
    ANTS_TAC;
      CONJ_TAC;
        FIRST_X_ASSUM_ST `periodic` MP_TAC THEN REWRITE_TAC[Oxl_def.periodic];
        BY(MESON_TAC[]);
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      MATCH_MP_TAC FUN_IN_IMAGE;
      BY(ASM_REWRITE_TAC[]);
    DISCH_TAC;
    EXPAND_TAC "V";
    REWRITE_TAC[IMAGE;IN_UNIV;SUBSET;IN_ELIM_THM];
    BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
  REWRITE_TAC[IN_IMAGE;IN_NUMSEG];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `?j. 0 <= j /\ j < k /\ x = i + j` (C SUBGOAL_THEN MP_TAC);
    TYPIFY `x - (i:num)` EXISTS_TAC;
    BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `!j. 2 <= j /\ j < k==> v (i + j) IN affine hull {vec 0,v i, v(i+k-1)}` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`j'`]);
    ANTS_TAC;
      BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    TYPIFY `aff_gt {vec 0,v i} {v (i+k-1)} SUBSET affine hull {vec 0,v i,v (i+k-1)}` ENOUGH_TO_SHOW_TAC;
      BY(SET_TAC[]);
    TYPIFY `{vec 0,v i,v (i+k-1)} = {vec 0,v i} UNION {v (i+k-1)}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    BY(REWRITE_TAC[ AFF_GT_SUBSET_AFFINE_HULL]);
  TYPIFY `{vec 0,v i, v (i+2)} SUBSET affine hull {vec 0, v i, v (i+k-1)}` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
        MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
        BY(SET_TAC[]);
      MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
      BY(SET_TAC[]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`(vec 0):real^3`;`v i`;`v (i+k-1)`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  DISCH_TAC;
  ASSUME_TAC (arith ` 2 <= j \/ j = 0 \/ j = 1` );
  REPEAT (POP_ASSUM DISJ_CASES_TAC);
      BY(ASM_MESON_TAC[]);
    ASM_REWRITE_TAC[arith `i + 0 = i`] THEN MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
    BY(SET_TAC[]);
  ASM_REWRITE_TAC[];
  (FIRST_X_ASSUM_ST `coplanar (a INSERT X)` MP_TAC);
  REWRITE_TAC[coplanar] THEN REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`u`;`v'`;`w'`];
  ANTS_TAC;
    CONJ_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[])
  ]);;
  (* }}} *)

let coplanar_aff_gt_simple = 
prove_by_refinement(
  `!s k v i.
    is_scs_v39 s /\ scs_k_v39 s = k /\
      3 < k /\ 
         MMs_v39 s v /\
      scs_basic_v39 s /\ 
	(!j. ~(v j = v i) ==> ~collinear {vec 0,v i,v j}) /\
	 coplanar {vec 0,v i, v(i+1),v(i+2)} ==>
      v (i+1) IN aff_gt {vec 0} {v i, v(i+2)}`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `~(k=0)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
  TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
  TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
  FIRST_ASSUM_ST `coplanar` MP_TAC;
  REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
  DISCH_TAC;
  TYPIFY `~coplanar ({vec 0} UNION V)` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "V";
    MATCH_MP_TAC Fektyiy.FEKTYIY;
    TYPIFY `s` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[IN]);
  TYPIFY `BBprime2_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Appendix.scs_basic;Ayqjtmd.unadorned_MMs]);
  TYPIFY `BBprime_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Appendix.BBprime2_v39]);
  TYPIFY `BBs_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Appendix.BBprime_v39]);
  INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`k`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `periodic v k /\ convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN ASM_MESON_TAC[arith `3 < k ==> ~(k<= 3)`]);
  INTRO_TAC Terminal.ITER_vv_rho_node1 [`v`;`k`];
  ASM_REWRITE_TAC[LET_THM];
  ASM_SIMP_TAC[arith `3 < k ==> 3 <= k`];
  DISCH_TAC;
  INTRO_TAC (GEN_ALL Odxlstcv2.CARD_V_EQ_SCS_K1) [`s`;`v`;`V`;`k`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    EXPAND_TAC "V";
    MATCH_MP_TAC FUN_IN_IMAGE;
    BY(REWRITE_TAC[IN_UNIV]);
  INTRO_TAC EGHNAVX_COLL_SCS [`s`;`k`;`v`;`i`];
  REWRITE_TAC[LET_THM];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `!a. 0 < a /\ (a:num) < k ==> ~(v i = v (i+a))` (C SUBGOAL_THEN ASSUME_TAC);
    TYPIFY `!i. v (i MOD k) = v i` (C SUBGOAL_THEN ASSUME_TAC);
      GEN_TAC;
      MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
      BY(ASM_MESON_TAC[arith `3 < k ==> ~(0=k)`]);
    FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
    GEN_TAC THEN DISCH_TAC;
    TYPIFY_GOAL_THEN `!i j. i < k /\ j < (k:num) /\ ~(i = j) ==> ~(v i = v j)` MATCH_MP_TAC;
      BY(ASM_MESON_TAC[]);
    REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC;
      BY(ASM_MESON_TAC[DIVISION]);
    TYPIFY `i MOD k = (i+0) MOD k` (C SUBGOAL_THEN SUBST1_TAC);
      BY(REWRITE_TAC[arith `i + 0 = i`]);
    GMATCH_SIMP_TAC Ocbicby.MOD_EQ_MOD_SHIFT;
    REPEAT (GMATCH_SIMP_TAC MOD_LT);
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
  FIRST_X_ASSUM DISJ_CASES_TAC;
    FIRST_X_ASSUM_ST `&0` (C INTRO_TAC [`2`;`2`]);
    NUM_REDUCE_TAC;
    ANTS_TAC;
      ASM_REWRITE_TAC[];
      BY(MATCH_MP_TAC (arith `3 < k ==> 2 < k`) THEN ASM_REWRITE_TAC[]);
    GMATCH_SIMP_TAC Local_lemmas1.COLL_AFF_GT_2_1;
    GMATCH_SIMP_TAC AFF_GT_1_2;
    REWRITE_TAC[IN_ELIM_THM;arith `t % vec 0 + a = a`];
    SUBCONJ_TAC;
      ONCE_REWRITE_TAC[DISJOINT_SYM];
      MATCH_MP_TAC Fan.th3a;
      ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,a,b}`] THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC);
      ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN FIRST_X_ASSUM MATCH_MP_TAC;
      BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
    DISCH_TAC;
    CONJ_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      ONCE_REWRITE_TAC[EQ_SYM_EQ];
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
    REPEAT WEAKER_STRIP_TAC;
    GEXISTL_TAC [`&1 + t2 / t3 - &1 / t3`;`-- t2 / t3`;`&1 / t3`];
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC REAL_LT_DIV;
    GMATCH_SIMP_TAC REAL_LT_DIV;
    ASM_REWRITE_TAC[arith `&0 < &1`];
    nCONJ_TAC 2;
      TYPIFY `--t2 / t3 % v i + &1 / t3 % (t2 % v i + t3 % v (i + 1)) = (-- t2 / t3 + (&1 / t3) * t2) % v i + ((&1 / t3)*t3) % v (i+1) ` (C SUBGOAL_THEN SUBST1_TAC);
        BY(VECTOR_ARITH_TAC);
      TYPIFY_GOAL_THEN `(--t2 / t3 + &1 / t3 * t2) = &0 /\ (&1 / t3 * t3 = &1)` (unlist REWRITE_TAC);
        BY(CONJ_TAC THEN Calc_derivative.CALC_ID_TAC THEN (REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC)) THEN REAL_ARITH_TAC);
      BY(VECTOR_ARITH_TAC);
    nCONJ_TAC 1;
      BY(Calc_derivative.CALC_ID_TAC THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    TYPIFY `~(&0 <= t2)` ENOUGH_TO_SHOW_TAC;
      BY(REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN MESON_TAC[arith `~(&0 <= t2) ==> &0 < -- t2`]);
    DISCH_TAC;
    INTRO_TAC (GEN_ALL Local_lemmas.FAN_IN_AFF_GE_IMP_EQ) [`V`;`E`;`(vec 0):real^3`;`v i`;`v (i+2)`;`v (i+1)`];
    ANTS_TAC;
      CONJ_TAC;
        MATCH_MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
        BY(ASM_REWRITE_TAC[]);
      CONJ_TAC;
        EXPAND_TAC "V";
        MATCH_MP_TAC FUN_IN_IMAGE;
        BY(REWRITE_TAC[IN_UNIV]);
      CONJ_TAC;
        EXPAND_TAC "E";
        BY(REWRITE_TAC[arith `i+1 = SUC i`;IN_IMAGE;IN_UNIV] THEN MESON_TAC[]);
      GMATCH_SIMP_TAC AFF_GE_1_2;
      REWRITE_TAC[IN_ELIM_THM];
      CONJ_TAC;
        ONCE_REWRITE_TAC[DISJOINT_SYM];
        MATCH_MP_TAC Fan.th3a;
        ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,a,b}`] THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC);
        ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN FIRST_X_ASSUM MATCH_MP_TAC;
        BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
      GEXISTL_TAC [`t1`;`t2`;`t3`];
      FIRST_X_ASSUM_ST `i+2` SUBST1_TAC;
      REWRITE_TAC[CONJ_ASSOC] THEN CONJ2_TAC;
        BY(VECTOR_ARITH_TAC);
      BY(REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    REWRITE_TAC[DE_MORGAN_THM];
    CONJ_TAC;
      ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN FIRST_X_ASSUM MATCH_MP_TAC;
      BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
    ONCE_REWRITE_TAC[EQ_SYM_EQ];
    MATCH_MP_TAC Hypermap_iso.fan_in_e_imp_neq;
    GEXISTL_TAC [`V`;`E`];
    CONJ_TAC;
      MATCH_MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
      BY(ASM_REWRITE_TAC[]);
    EXPAND_TAC "E";
    BY(REWRITE_TAC[arith `i+2 = SUC (i+1)`;IN_IMAGE;IN_UNIV] THEN MESON_TAC[]);
  COMMENT "second disj";
  FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`2`]);
  FIRST_X_ASSUM_ST `aff_gt` kill;
  FIRST_X_ASSUM_ST `0 < a` MP_TAC THEN BURY_MP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`2`;`k-1`]);
  ANTS_TAC;
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  DISCH_TAC;
  TYPIFY_GOAL_THEN `azim (vec 0) (v i) (v (i + 1)) (v (i + 2)) =      azim (vec 0) (v i) (v (i + 1)) (v (i + k - 1))` (unlist REWRITE_TAC);
    BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  DISCH_TAC;
  PROOF_BY_CONTR_TAC;
  TYPIFY `V SUBSET affine hull {vec 0,v i,v (i+k-1)}` ENOUGH_TO_SHOW_TAC;
    DISCH_TAC THEN FIRST_X_ASSUM_ST `coplanar` MP_TAC THEN REWRITE_TAC[coplanar];
    GEXISTL_TAC [`(vec 0):real^3`;`v i`;`v (i+k-1)`];
    FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_UNION;IN_SING];
    TYPIFY `vec 0 IN affine hull {vec 0,v i ,v(i+k-1)}` ENOUGH_TO_SHOW_TAC;
      BY(MESON_TAC[]);
    MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
    BY(SET_TAC[]);
  TYPIFY `!w. w IN IMAGE v (i..i + k - 1) ==> w IN affine hull {vec 0,v i , v(i+k-1)}` ENOUGH_TO_SHOW_TAC;
    GMATCH_SIMP_TAC (GSYM Oxl_2012.PERIODIC_IMAGE_EQUAL);
    ASM_REWRITE_TAC[];
    DISCH_TAC;
    INTRO_TAC Oxl_def.periodic_numseg [`(\j. v j IN affine hull {vec 0,v i,v (i+k-1)})`;`k`];
    ASM_REWRITE_TAC[];
    ANTS_TAC;
      CONJ_TAC;
        FIRST_X_ASSUM_ST `periodic` MP_TAC THEN REWRITE_TAC[Oxl_def.periodic];
        BY(MESON_TAC[]);
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      MATCH_MP_TAC FUN_IN_IMAGE;
      BY(ASM_REWRITE_TAC[]);
    DISCH_TAC;
    EXPAND_TAC "V";
    REWRITE_TAC[IMAGE;IN_UNIV;SUBSET;IN_ELIM_THM];
    BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
  REWRITE_TAC[IN_IMAGE;IN_NUMSEG];
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `?j. 0 <= j /\ j < k /\ x = i + j` (C SUBGOAL_THEN MP_TAC);
    TYPIFY `x - (i:num)` EXISTS_TAC;
    BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  ASM_REWRITE_TAC[];
  TYPIFY `!j. 2 <= j /\ j < k==> v (i + j) IN affine hull {vec 0,v i, v(i+k-1)}` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`j'`]);
    ANTS_TAC;
      BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
    TYPIFY `aff_gt {vec 0,v i} {v (i+k-1)} SUBSET affine hull {vec 0,v i,v (i+k-1)}` ENOUGH_TO_SHOW_TAC;
      BY(SET_TAC[]);
    TYPIFY `{vec 0,v i,v (i+k-1)} = {vec 0,v i} UNION {v (i+k-1)}` (C SUBGOAL_THEN SUBST1_TAC);
      BY(SET_TAC[]);
    BY(REWRITE_TAC[ AFF_GT_SUBSET_AFFINE_HULL]);
  TYPIFY `{vec 0,v i, v (i+2)} SUBSET affine hull {vec 0, v i, v (i+k-1)}` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
        MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
        BY(SET_TAC[]);
      MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
      BY(SET_TAC[]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`(vec 0):real^3`;`v i`;`v (i+k-1)`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    ONCE_REWRITE_TAC[EQ_SYM_EQ];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`(vec 0):real^3`;`v i`;`v (i+k-1)`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    ONCE_REWRITE_TAC[EQ_SYM_EQ];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  DISCH_TAC;
  ASSUME_TAC (arith ` 2 <= j \/ j = 0 \/ j = 1` );
  REPEAT (POP_ASSUM DISJ_CASES_TAC);
      BY(ASM_MESON_TAC[]);
    ASM_REWRITE_TAC[arith `i + 0 = i`] THEN MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
    BY(SET_TAC[]);
  ASM_REWRITE_TAC[];
  (FIRST_X_ASSUM_ST `coplanar (a INSERT X)` MP_TAC);
  REWRITE_TAC[coplanar] THEN REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`u`;`v'`;`w'`];
  ANTS_TAC;
    CONJ_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    ONCE_REWRITE_TAC[EQ_SYM_EQ];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
  BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[])
  ]);;
  (* }}} *)

(*
let a5_assumption_reduction = prove_by_refinement(
  `!s f v e.
    is_scs_v39 s /\
    scs_k_v39 s  = 5 /\
    BBs_v39 s v /\
    (!i j. scs_diag 5 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
    deformation f (IMAGE v (:num)) (--e,e) /\
    (!w t. ~(w = v 0) /\ ~(w = v 1)  ==> (f w t = w)) /\
    (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 1) t,v 2) = dist(v 1,v 2) /\ dist(f (v 0) t,v 4) = dist(v 0,v 4))) /\
    (?e1. &0 < e1 /\ (!t. abs t < e1 ==> scs_a_v39 s 0 1 <= dist(f (v 0) t,f (v 1) t)))
    ==>
    (!i j. ?e1. &0 < e1 /\ (scs_a_v39 s i j = dist(v i,v j) ==> 
	(!t. abs t < e1 ==> scs_a_v39 s i j <= dist(f (v i) t,f (v j) t))))
    `,
  (* {{{ proof *)
  [
  REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC Cuxvzoz.I_IMP THEN ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
  TYPIFY `!i j.scs_a_v39 s (i MOD 5) (j MOD 5) = scs_a_v39 s i j  /\ scs_b_v39 s (i MOD 5) (j MOD 5) = scs_b_v39 s i j ` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC;
    ASM_REWRITE_TAC[Appendix.is_scs_v39];
    REPEAT WEAKER_STRIP_TAC;
    BY(REPEAT (FIRST_X_ASSUM_ST `periodic2` MP_TAC) THEN MESON_TAC[Cuxvzoz.periodic2_MOD;arith `~(5 = 0)`]);
  TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
  TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
    BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
  INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `!j. j < 5 ==> (j MOD 5 = j)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[MOD_LT]);
  COMMENT "scs_a_v39";
  REWRITE_TAC[I_THM];
  MATCH_MP_TAC Terminal.periodic2_mod_reduce;
  TYPIFY `5` EXISTS_TAC;
  ASM_REWRITE_TAC[arith `~(5=0)`];
  CONJ_TAC;
    MATCH_MP_TAC Cuxvzoz.MOD_periodic2;
    BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[] THEN MESON_TAC[arith `~(5=0)`]);
  TYPIFY_GOAL_THEN `!P. (!i j. P i j ==> P j i) /\ (!i j. (i <= (j:num)) ==> P i j) ==> (!i j. P i j)` MATCH_MP_TAC;
    BY(MESON_TAC[arith `i <= j \/ j <= (i:num)`]);
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    ONCE_REWRITE_TAC[DIST_SYM];
    TYPIFY `scs_a_v39 s j i = scs_a_v39 s i j` (C SUBGOAL_THEN SUBST1_TAC);
      FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC THEN REWRITE_TAC[Appendix.is_scs_v39] THEN REPEAT WEAKER_STRIP_TAC;
      BY(ASM_MESON_TAC[]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `!t. f (v 2) t = v 2 /\ f (v 3) t = v 3 /\ f (v 4) t = v 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[arith `0 < 5 /\ 1 < 5 /\ 2 < 5 /\ 3 < 5 /\ 4 < 5 /\ ~(2 = 0) /\ ~(2 = 1) /\ ~(3 = 0) /\ ~(3 = 1) /\ ~(4 =0) /\ ~(4=1)`]);
  REWRITE_TAC[arith `i < 5 <=> (i = 0) \/ (i = 1) \/ (i=2) \/ (i  =3) \/ (i=4)`];
  TYPIFY `scs_diag 5 0 2 /\ scs_diag 5 0 3 /\ scs_diag 5 1 3 /\ scs_diag 5 1 4 /\ scs_diag 5 2 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
  ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
  TYPIFY `!i j. scs_diag 5 i j ==> (?e1. &0 < e1 /\               (scs_a_v39 s i j = dist (v i,v j)                ==> (!t. abs t < e1                         ==> scs_a_v39 s i j <= dist (f (v i) t,f (v j) t))))` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[arith `x < y ==> ~(x = y)`]);
  TYPIFY `!i. T ==> (?e1. &0 < e1 /\               (scs_a_v39 s i i = dist (v i,v i)                ==> (!t. abs t < e1                         ==> scs_a_v39 s i i <= dist (f (v i) t,f (v i) t))))` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[DIST_REFL];
    BY(MESON_TAC[arith `x = &0 ==> x <= &0`;arith `&0 < &1`]);
  REPEAT GEN_TAC;
  TYPIFY `(?e1. &0 < e1 /\                    (scs_a_v39 s 0 1 = dist (v 0,v 1)                     ==> (!t. abs t < e1                              ==> scs_a_v39 s 0 1 <=                                  dist (f (v 0) t,f (v 1) t)))) /\     (?e1. &0 < e1 /\                    (scs_a_v39 s 1 2 = dist (v 1,v 2)                     ==> (!t. abs t < e1                              ==> scs_a_v39 s 1 2 <=                                  dist (f (v 1) t,f (v 2) t)))) /\     (?e1. &0 < e1 /\                    (scs_a_v39 s 2 3 = dist (v 2,v 3)                     ==> (!t. abs t < e1                              ==> scs_a_v39 s 2 3 <=                                  dist (f (v 2) t,f (v 3) t)))) /\     (?e1. &0 < e1 /\                    (scs_a_v39 s 3 4 = dist (v 3,v 4)                     ==> (!t. abs t < e1                              ==> scs_a_v39 s 3 4 <=                                  dist (f (v 3) t,f (v 4) t)))) /\      (?e1. &0 < e1 /\                    (scs_a_v39 s 0 4 = dist (v 0,v 4)                     ==> (!t. abs t < e1                              ==> scs_a_v39 s 0 4 <=                                  dist (f (v 0) t,f (v 4) t))))` (C SUBGOAL_THEN MP_TAC);
    ASM_REWRITE_TAC[];
    TYPIFY_GOAL_THEN `!a b. (?e1. &0 < e1 /\ (a = b ==> (!t. abs t < e1 ==> a <= b)))` (unlist REWRITE_TAC);
      BY(MESON_TAC[arith `&0 < &1`;arith `(a = b) ==> (a <= b)`]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[]);
    BY(ASM_MESON_TAC[arith `x = y ==> x <= y`]);
  REWRITE_TAC[LEFT_OR_DISTRIB;RIGHT_OR_DISTRIB;GSYM DISJ_ASSOC];
  ONCE_REWRITE_TAC[TAUT `(a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ((T ==> a1) /\ (T ==> a2) /\ (T ==> a3) /\ (T ==> a4) /\ (T ==> a5))`];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN FIRST_X_ASSUM (unlist REWRITE_TAC) THEN NUM_REDUCE_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)
*)

let a5_assumption_reduction = 
prove_by_refinement(
  `!s f v e.
    is_scs_v39 s /\
    scs_k_v39 s  = 5 /\
    BBs_v39 s v /\
    (!i j. scs_diag 5 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
    deformation f (IMAGE v (:num)) (--e,e) /\
    (!w t. ~(w = v 4) /\ ~(w = v 0)  ==> (f w t = w)) /\
    (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 4) t,f (v 0) t) = dist(v 4,v 0) /\ dist(f (v 4) t,v 3) = dist(v 4,v 3))) /\
    (?e1. &0 < e1 /\ (!t. abs t < e1 ==> scs_a_v39 s 0 1 <= dist(f (v 0) t,v 1)))
    ==>
    (!i j. ?e1. &0 < e1 /\ (scs_a_v39 s i j = dist(v i,v j) ==> 
	(!t. abs t < e1 ==> scs_a_v39 s i j <= dist(f (v i) t,f (v j) t))))
    `,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC Cuxvzoz.I_IMP THEN ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
  TYPIFY `!i j.scs_a_v39 s (i MOD 5) (j MOD 5) = scs_a_v39 s i j  /\ scs_b_v39 s (i MOD 5) (j MOD 5) = scs_b_v39 s i j ` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC;
    ASM_REWRITE_TAC[Appendix.is_scs_v39];
    REPEAT WEAKER_STRIP_TAC;
    BY(REPEAT (FIRST_X_ASSUM_ST `periodic2` MP_TAC) THEN MESON_TAC[Cuxvzoz.periodic2_MOD;arith `~(5 = 0)`]);
  TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
  TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
    BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
  INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `!j. j < 5 ==> (j MOD 5 = j)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[MOD_LT]);
  COMMENT "scs_a_v39";
  REWRITE_TAC[I_THM];
  MATCH_MP_TAC Terminal.periodic2_mod_reduce;
  TYPIFY `5` EXISTS_TAC;
  ASM_REWRITE_TAC[arith `~(5=0)`];
  CONJ_TAC;
    MATCH_MP_TAC Cuxvzoz.MOD_periodic2;
    BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[] THEN MESON_TAC[arith `~(5=0)`]);
  TYPIFY_GOAL_THEN `!P. (!i j. P i j ==> P j i) /\ (!i j. (i <= (j:num)) ==> P i j) ==> (!i j. P i j)` MATCH_MP_TAC;
    BY(MESON_TAC[arith `i <= j \/ j <= (i:num)`]);
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    ONCE_REWRITE_TAC[DIST_SYM];
    TYPIFY `scs_a_v39 s j i = scs_a_v39 s i j` (C SUBGOAL_THEN SUBST1_TAC);
      FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC THEN REWRITE_TAC[Appendix.is_scs_v39] THEN REPEAT WEAKER_STRIP_TAC;
      BY(ASM_MESON_TAC[]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i=j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[]);
  TYPIFY `!t. f (v 2) t = v 2 /\ f (v 3) t = v 3 /\ f (v 1) t = v 1` (C SUBGOAL_THEN ASSUME_TAC);
    BY(GEN_TAC THEN REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC) THEN NUM_REDUCE_TAC);
  REWRITE_TAC[arith `i < 5 <=> (i = 0) \/ (i = 1) \/ (i=2) \/ (i  =3) \/ (i=4)`];
  TYPIFY `scs_diag 5 0 2 /\ scs_diag 5 0 3 /\ scs_diag 5 1 3 /\ scs_diag 5 1 4 /\ scs_diag 5 2 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
  ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
  TYPIFY `!i j. scs_diag 5 i j ==> (?e1. &0 < e1 /\               (scs_a_v39 s i j = dist (v i,v j)                ==> (!t. abs t < e1                         ==> scs_a_v39 s i j <= dist (f (v i) t,f (v j) t))))` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[arith `x < y ==> ~(x = y)`]);
  TYPIFY `!i. T ==> (?e1. &0 < e1 /\               (scs_a_v39 s i i = dist (v i,v i)                ==> (!t. abs t < e1                         ==> scs_a_v39 s i i <= dist (f (v i) t,f (v i) t))))` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[DIST_REFL];
    BY(MESON_TAC[arith `x = &0 ==> x <= &0`;arith `&0 < &1`]);
  REPEAT GEN_TAC;
  TYPIFY `(?e1. &0 < e1 /\                    (scs_a_v39 s 0 1 = dist (v 0,v 1)                     ==> (!t. abs t < e1                              ==> scs_a_v39 s 0 1 <=                                  dist (f (v 0) t,f (v 1) t)))) /\     (?e1. &0 < e1 /\                    (scs_a_v39 s 1 2 = dist (v 1,v 2)                     ==> (!t. abs t < e1                              ==> scs_a_v39 s 1 2 <=                                  dist (f (v 1) t,f (v 2) t)))) /\     (?e1. &0 < e1 /\                    (scs_a_v39 s 2 3 = dist (v 2,v 3)                     ==> (!t. abs t < e1                              ==> scs_a_v39 s 2 3 <=                                  dist (f (v 2) t,f (v 3) t)))) /\     (?e1. &0 < e1 /\                    (scs_a_v39 s 3 4 = dist (v 3,v 4)                     ==> (!t. abs t < e1                              ==> scs_a_v39 s 3 4 <=                                  dist (f (v 3) t,f (v 4) t)))) /\      (?e1. &0 < e1 /\                    (scs_a_v39 s 0 4 = dist (v 0,v 4)                     ==> (!t. abs t < e1                              ==> scs_a_v39 s 0 4 <=                                  dist (f (v 0) t,f (v 4) t))))` (C SUBGOAL_THEN MP_TAC);
    ASM_REWRITE_TAC[];
    TYPIFY_GOAL_THEN `!a b. (?e1. &0 < e1 /\ (a = b ==> (!t. abs t < e1 ==> a <= b)))` (unlist REWRITE_TAC);
      BY(MESON_TAC[arith `&0 < &1`;arith `(a = b) ==> (a <= b)`]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[]);
    ONCE_REWRITE_TAC[DIST_SYM];
    BY(ASM_MESON_TAC[arith `x = y ==> x <= y`]);
  REWRITE_TAC[LEFT_OR_DISTRIB;RIGHT_OR_DISTRIB;GSYM DISJ_ASSOC];
  ONCE_REWRITE_TAC[TAUT `(a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ((T ==> a1) /\ (T ==> a2) /\ (T ==> a3) /\ (T ==> a4) /\ (T ==> a5))`];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN FIRST_X_ASSUM (unlist REWRITE_TAC) THEN NUM_REDUCE_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

(*
let b5_assumption_reduction = prove_by_refinement(
  `!s f v e.
    is_scs_v39 s /\
    scs_k_v39 s  = 5 /\
    BBs_v39 s v /\
    (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 s i j) /\
    deformation f (IMAGE v (:num)) (--e,e) /\
    (!w t. ~(w = v 0) /\ ~(w = v 1)  ==> (f w t = w)) /\
    (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 1) t,v 2) = dist(v 1,v 2) /\ dist(f (v 0) t,v 4) = dist(v 0,v 4))) /\
    (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 0) t,f (v 1) t) <= dist(v 0, v 1)))
    ==>
    (!i j. ?e1. &0 < e1 /\ (dist(v i,v j) = scs_b_v39 s i j ==> 
	(!t. abs t < e1 ==> dist(f (v i) t,f (v j) t) <= scs_b_v39 s i j)))
    `,
  (* {{{ proof *)
  [
  REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC Cuxvzoz.I_IMP THEN ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
  TYPIFY `!i j.scs_a_v39 s (i MOD 5) (j MOD 5) = scs_a_v39 s i j  /\ scs_b_v39 s (i MOD 5) (j MOD 5) = scs_b_v39 s i j ` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC;
    ASM_REWRITE_TAC[Appendix.is_scs_v39];
    REPEAT WEAKER_STRIP_TAC;
    BY(REPEAT (FIRST_X_ASSUM_ST `periodic2` MP_TAC) THEN MESON_TAC[Cuxvzoz.periodic2_MOD;arith `~(5 = 0)`]);
  TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
  TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
    BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
  INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `!j. j < 5 ==> (j MOD 5 = j)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[MOD_LT]);
  COMMENT "scs_b_v39";
  REWRITE_TAC[I_THM];
  MATCH_MP_TAC Terminal.periodic2_mod_reduce;
  TYPIFY `5` EXISTS_TAC;
  ASM_REWRITE_TAC[arith `~(5=0)`];
  CONJ_TAC;
    MATCH_MP_TAC Cuxvzoz.MOD_periodic2;
    BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[] THEN MESON_TAC[arith `~(5=0)`]);
  TYPIFY_GOAL_THEN `!P. (!i j. P i j ==> P j i) /\ (!i j. (i <= (j:num)) ==> P i j) ==> (!i j. P i j)` MATCH_MP_TAC;
    BY(MESON_TAC[arith `i <= j \/ j <= (i:num)`]);
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    ONCE_REWRITE_TAC[DIST_SYM];
    TYPIFY `scs_b_v39 s j i = scs_b_v39 s i j` (C SUBGOAL_THEN SUBST1_TAC);
      FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC THEN REWRITE_TAC[Appendix.is_scs_v39] THEN REPEAT WEAKER_STRIP_TAC;
      BY(ASM_MESON_TAC[]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `!t. f (v 2) t = v 2 /\ f (v 3) t = v 3 /\ f (v 4) t = v 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[arith `0 < 5 /\ 1 < 5 /\ 2 < 5 /\ 3 < 5 /\ 4 < 5 /\ ~(2 = 0) /\ ~(2 = 1) /\ ~(3 = 0) /\ ~(3 = 1) /\ ~(4 =0) /\ ~(4=1)`]);
  TYPIFY `scs_diag 5 0 2 /\ scs_diag 5 0 3 /\ scs_diag 5 1 3 /\ scs_diag 5 1 4 /\ scs_diag 5 2 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
  TYPIFY `!i j. scs_diag 5 i j ==> (?e1. &0 < e1 /\               (dist (v i,v j) = scs_b_v39 s i j                ==> (!t. abs t < e1                         ==> dist (f (v i) t,f (v j) t) <= scs_b_v39 s i j)))` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `&1` EXISTS_TAC;
    (REWRITE_TAC[arith `&0 < &1`]);
    TYPIFY `dist(v i,v j) <= &4 * h0` ENOUGH_TO_SHOW_TAC;
      FIRST_X_ASSUM_ST `&4 * h0` (C INTRO_TAC [`i`;`j`]);
      ASM_REWRITE_TAC[];
      BY(REAL_ARITH_TAC);
    INTRO_TAC DIST_TRIANGLE [`v i`;`(vec 0):real^3`;`v j`];
    REWRITE_TAC[DIST_0];
    TYPIFY `!i. norm (v i) <= &2 * h0` ENOUGH_TO_SHOW_TAC;
      BY(DISCH_TAC THEN FIRST_ASSUM (C INTRO_TAC [`i`]) THEN FIRST_X_ASSUM (C INTRO_TAC [`j`]) THEN REAL_ARITH_TAC);
    FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN REPEAT WEAKER_STRIP_TAC;
    BY(FIRST_X_ASSUM_ST `ball_annulus` MP_TAC THEN REWRITE_TAC[Terminal.IMAGE_SUBSET_IN;IN_UNIV] THEN MESON_TAC[Fnjlbxs.in_ball_annulus]);
  TYPIFY `!i. T ==> (?e1. &0 < e1 /\               (dist (v i,v i) = scs_b_v39 s i i                ==> (!t. abs t < e1                         ==> dist (f (v i) t,f (v i) t) <= scs_b_v39 s i i)))` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[DIST_REFL];
    BY(MESON_TAC[arith `x = &0 ==> x <= &0`;arith `&0 < &1`]);
  REPEAT GEN_TAC;
  TYPIFY `(?e1. &0 < e1 /\           (dist (v 0,v 1) = scs_b_v39 s 0 1            ==> (!t. abs t < e1                     ==> dist (f (v 0) t,f (v 1) t) <= scs_b_v39 s 0 1))) /\(?e1. &0 < e1 /\           (dist (v 1,v 2) = scs_b_v39 s 1 2            ==> (!t. abs t < e1                     ==> dist (f (v 1) t,f (v 2) t) <= scs_b_v39 s 1 2))) /\(?e1. &0 < e1 /\           (dist (v 2,v 3) = scs_b_v39 s 2 3            ==> (!t. abs t < e1                     ==> dist (f (v 2) t,f (v 3) t) <= scs_b_v39 s 2 3))) /\(?e1. &0 < e1 /\           (dist (v 3,v 4) = scs_b_v39 s 3 4            ==> (!t. abs t < e1                     ==> dist (f (v 3) t,f (v 4) t) <= scs_b_v39 s 3 4))) /\(?e1. &0 < e1 /\           (dist (v 0,v 4) = scs_b_v39 s 0 4            ==> (!t. abs t < e1                     ==> dist (f (v 0) t,f (v 4) t) <= scs_b_v39 s 0 4)))` (C SUBGOAL_THEN MP_TAC);
    ASM_REWRITE_TAC[];
    TYPIFY_GOAL_THEN `!a b. (?e1. &0 < e1 /\ (a = b ==> (!t. abs t < e1 ==> a <= b)))` (unlist REWRITE_TAC);
      BY(MESON_TAC[arith `&0 < &1`;arith `(a = b) ==> (a <= b)`]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[]);
    BY(ASM_MESON_TAC[arith `x = y ==> x <= y`]);
  DISCH_TAC;
  REWRITE_TAC[arith `i < 5 <=> (i = 0) \/ (i = 1) \/ (i=2) \/ (i  =3) \/ (i=4)`];
  ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
  REWRITE_TAC[LEFT_OR_DISTRIB;RIGHT_OR_DISTRIB;GSYM DISJ_ASSOC];
  FIRST_X_ASSUM MP_TAC;
  ONCE_REWRITE_TAC[TAUT `(a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ((T ==> a1) /\ (T ==> a2) /\ (T ==> a3) /\ (T ==> a4) /\ (T ==> a5))`];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN FIRST_X_ASSUM (unlist REWRITE_TAC) THEN NUM_REDUCE_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)
*)

let b5_assumption_reduction = 
prove_by_refinement(
  `!s f v e.
    is_scs_v39 s /\
    scs_k_v39 s  = 5 /\
    BBs_v39 s v /\
    (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 s i j) /\
    deformation f (IMAGE v (:num)) (--e,e) /\
    (!w t. ~(w = v 4) /\ ~(w = v 0)  ==> (f w t = w)) /\
    (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 4) t,f (v 0) t) = dist(v 4,v 0) /\ dist(f (v 4) t,v 3) = dist(v 4,v 3))) /\
    (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 0) t, (v 1)) <= dist(v 0, v 1)))
    ==>
    (!i j. ?e1. &0 < e1 /\ (dist(v i,v j) = scs_b_v39 s i j ==> 
	(!t. abs t < e1 ==> dist(f (v i) t,f (v j) t) <= scs_b_v39 s i j)))
    `,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC Cuxvzoz.I_IMP THEN ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
  TYPIFY `!i j.scs_a_v39 s (i MOD 5) (j MOD 5) = scs_a_v39 s i j  /\ scs_b_v39 s (i MOD 5) (j MOD 5) = scs_b_v39 s i j ` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC;
    ASM_REWRITE_TAC[Appendix.is_scs_v39];
    REPEAT WEAKER_STRIP_TAC;
    BY(REPEAT (FIRST_X_ASSUM_ST `periodic2` MP_TAC) THEN MESON_TAC[Cuxvzoz.periodic2_MOD;arith `~(5 = 0)`]);
  TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
  TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
    BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
  INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `!j. j < 5 ==> (j MOD 5 = j)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[MOD_LT]);
  COMMENT "scs_b_v39";
  REWRITE_TAC[I_THM];
  MATCH_MP_TAC Terminal.periodic2_mod_reduce;
  TYPIFY `5` EXISTS_TAC;
  ASM_REWRITE_TAC[arith `~(5=0)`];
  CONJ_TAC;
    MATCH_MP_TAC Cuxvzoz.MOD_periodic2;
    BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[] THEN MESON_TAC[arith `~(5=0)`]);
  TYPIFY_GOAL_THEN `!P. (!i j. P i j ==> P j i) /\ (!i j. (i <= (j:num)) ==> P i j) ==> (!i j. P i j)` MATCH_MP_TAC;
    BY(MESON_TAC[arith `i <= j \/ j <= (i:num)`]);
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    ONCE_REWRITE_TAC[DIST_SYM];
    TYPIFY `scs_b_v39 s j i = scs_b_v39 s i j` (C SUBGOAL_THEN SUBST1_TAC);
      FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC THEN REWRITE_TAC[Appendix.is_scs_v39] THEN REPEAT WEAKER_STRIP_TAC;
      BY(ASM_MESON_TAC[]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i=j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[]);
  TYPIFY `!t. f (v 2) t = v 2 /\ f (v 3) t = v 3 /\ f (v 1) t = v 1` (C SUBGOAL_THEN ASSUME_TAC);
    BY(GEN_TAC THEN REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC) THEN NUM_REDUCE_TAC);
  TYPIFY `scs_diag 5 0 2 /\ scs_diag 5 0 3 /\ scs_diag 5 1 3 /\ scs_diag 5 1 4 /\ scs_diag 5 2 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
  TYPIFY `!i j. scs_diag 5 i j ==> (?e1. &0 < e1 /\               (dist (v i,v j) = scs_b_v39 s i j                ==> (!t. abs t < e1                         ==> dist (f (v i) t,f (v j) t) <= scs_b_v39 s i j)))` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `&1` EXISTS_TAC;
    (REWRITE_TAC[arith `&0 < &1`]);
    TYPIFY `dist(v i,v j) <= &4 * h0` ENOUGH_TO_SHOW_TAC;
      FIRST_X_ASSUM_ST `&4 * h0` (C INTRO_TAC [`i`;`j`]);
      ASM_REWRITE_TAC[];
      BY(REAL_ARITH_TAC);
    INTRO_TAC DIST_TRIANGLE [`v i`;`(vec 0):real^3`;`v j`];
    REWRITE_TAC[DIST_0];
    TYPIFY `!i. norm (v i) <= &2 * h0` ENOUGH_TO_SHOW_TAC;
      BY(DISCH_TAC THEN FIRST_ASSUM (C INTRO_TAC [`i`]) THEN FIRST_X_ASSUM (C INTRO_TAC [`j`]) THEN REAL_ARITH_TAC);
    FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN REPEAT WEAKER_STRIP_TAC;
    BY(FIRST_X_ASSUM_ST `ball_annulus` MP_TAC THEN REWRITE_TAC[Terminal.IMAGE_SUBSET_IN;IN_UNIV] THEN MESON_TAC[Fnjlbxs.in_ball_annulus]);
  TYPIFY `!i. T ==> (?e1. &0 < e1 /\               (dist (v i,v i) = scs_b_v39 s i i                ==> (!t. abs t < e1                         ==> dist (f (v i) t,f (v i) t) <= scs_b_v39 s i i)))` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[DIST_REFL];
    BY(MESON_TAC[arith `x = &0 ==> x <= &0`;arith `&0 < &1`]);
  REPEAT GEN_TAC;
  TYPIFY `(?e1. &0 < e1 /\           (dist (v 0,v 1) = scs_b_v39 s 0 1            ==> (!t. abs t < e1                     ==> dist (f (v 0) t,f (v 1) t) <= scs_b_v39 s 0 1))) /\(?e1. &0 < e1 /\           (dist (v 1,v 2) = scs_b_v39 s 1 2            ==> (!t. abs t < e1                     ==> dist (f (v 1) t,f (v 2) t) <= scs_b_v39 s 1 2))) /\(?e1. &0 < e1 /\           (dist (v 2,v 3) = scs_b_v39 s 2 3            ==> (!t. abs t < e1                     ==> dist (f (v 2) t,f (v 3) t) <= scs_b_v39 s 2 3))) /\(?e1. &0 < e1 /\           (dist (v 3,v 4) = scs_b_v39 s 3 4            ==> (!t. abs t < e1                     ==> dist (f (v 3) t,f (v 4) t) <= scs_b_v39 s 3 4))) /\(?e1. &0 < e1 /\           (dist (v 0,v 4) = scs_b_v39 s 0 4            ==> (!t. abs t < e1                     ==> dist (f (v 0) t,f (v 4) t) <= scs_b_v39 s 0 4)))` (C SUBGOAL_THEN MP_TAC);
    ASM_REWRITE_TAC[];
    TYPIFY_GOAL_THEN `!a b. (?e1. &0 < e1 /\ (a = b ==> (!t. abs t < e1 ==> a <= b)))` (unlist REWRITE_TAC);
      BY(MESON_TAC[arith `&0 < &1`;arith `(a = b) ==> (a <= b)`]);
    CONJ_TAC;
      BY(ASM_MESON_TAC[]);
    REPEAT (FIRST_X_ASSUM_ST `dist(v 4,v 0)` MP_TAC);
    REWRITE_TAC[DIST_SYM];
    BY(ASM_MESON_TAC[arith `x = y ==> x <= y`]);
  DISCH_TAC;
  REWRITE_TAC[arith `i < 5 <=> (i = 0) \/ (i = 1) \/ (i=2) \/ (i  =3) \/ (i=4)`];
  ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
  REWRITE_TAC[LEFT_OR_DISTRIB;RIGHT_OR_DISTRIB;GSYM DISJ_ASSOC];
  FIRST_X_ASSUM MP_TAC;
  ONCE_REWRITE_TAC[TAUT `(a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ((T ==> a1) /\ (T ==> a2) /\ (T ==> a3) /\ (T ==> a4) /\ (T ==> a5))`];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN FIRST_X_ASSUM (unlist REWRITE_TAC) THEN NUM_REDUCE_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

(* was dihV_dih_y *)

let azim_dih_y = 
prove_by_refinement(
  `!v0 v1 v2 v3. ~collinear {v0,v1,v2} /\ ~collinear{v0,v1,v3} /\ azim v0 v1 v2 v3 <= pi ==>
    azim v0 v1 v2 v3 = dih_y (dist(v0,v1)) (dist(v0,v2)) (dist(v0,v3))
      (dist(v2,v3)) (dist(v1,v3)) (dist(v1,v2))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC AZIM_DIHV_SAME_STRONG [`v0`;`v1`;`v2`;`v3`];
  ASM_REWRITE_TAC[];
  DISCH_THEN SUBST1_TAC;
  GMATCH_SIMP_TAC (REWRITE_RULE[LET_THM] Merge_ineq.DIHV_DIH_X);
  REWRITE_TAC[Sphere.dih_y;LET_THM;arith `x*x = x pow 2`];
  BY(ASM_REWRITE_TAC[GSYM Collect_geom2.NOT_COL_EQ_UPS_X_POS])
  ]);;
  (* }}} *)

(* next azim reduction *)

(*
let azm5_reduction = prove_by_refinement(
 `!s f v e.
     is_scs_v39 s /\
     scs_k_v39 s = 5 /\
     BBs_v39 s v /\
     scs_generic v /\
     deformation f (IMAGE v (:num)) (--e,e) /\
     (!w t. ~(w = v 0) /\ ~(w = v 4) ==> f w t = w) /\
     azim (vec 0) (v 0) (v 1) (v 4) < pi /\
     azim (vec 0) (v 1) (v 2) (v 0) < pi /\
     &0 < azim (vec 0) (v 0) (v 1) (v 3) /\
     (?e1. &0 < e1 /\
           (!t. abs t < e1
                ==> azim (vec 0) (v 3) (f (v 0) t) (v 1) <=
                    azim (vec 0) (v 3) (v 0) (v 1))) /\
     (?e1. &0 < e1 /\
           (!t. abs t < e1
	          // make this a dih_y condition?? 
                ==> azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) =
                    azim (vec 0) (v 3) (v 4) (v 0) /\
                    azim (vec 0) (f (v 4) t) (f (v 0) t) (v 3) =
                    azim (vec 0) (v 4) (v 0) (v 3) /\
                    azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) =
                    azim (vec 0) (v 0) (v 3) (v 4)))
     ==> azim (vec 0) (v 3) (v 4) (v 2) =
         azim (vec 0) (v 3) (v 4) (v 0) +
         azim (vec 0) (v 3) (v 0) (v 1) +
         azim (vec 0) (v 3) (v 1) (v 2) /\
         azim (vec 0) (v 0) (v 1) (v 4) =
         azim (vec 0) (v 0) (v 1) (v 3) + azim (vec 0) (v 0) (v 3) (v 4) /\
         azim (vec 0) (v 1) (v 2) (v 0) =
         azim (vec 0) (v 1) (v 2) (v 3) + azim (vec 0) (v 1) (v 3) (v 0) /\
         (?e1. &0 < e1 /\
               (!t. abs t < e1
                    ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) =
                        azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) +
                        azim (vec 0) (v 3) (f (v 0) t) (v 1) +
                        azim (vec 0) (v 3) (v 1) (v 2) /\
                        azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) =
                        azim (vec 0) (f (v 0) t) (v 1) (v 3) +
                        azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) /\
                        azim (vec 0) (v 1) (v 2) (f (v 0) t) =
                        azim (vec 0) (v 1) (v 2) (v 3) +
                        azim (vec 0) (v 1) (v 3) (f (v 0) t) /\
		        &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\
		        azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi)) /\
         (!i. ?e0. &0 < e0 /\
                   (azim (vec 0) (v i) (v (i + 1)) (v (i + 4)) = pi
                    ==> (!t. abs t < e0
                             ==> azim (vec 0) (f (v i) t) (f (v (i + 1)) t)
                                 (f (v (i + 4)) t) <=
                                 pi)))`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  ASSUME_TAC (arith `~(0 = 5)`);
  TYPIFY `!i. i MOD 5 < 5` (C SUBGOAL_THEN ASSUME_TAC);
    BY((FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[DIVISION]);
  TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
  TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
    BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
  TYPIFY `v 5 = v 0 /\ v 6 = v 1 /\ v 7 = v 2 /\ v 8 = v 3 /\ v 9  = v 4` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
    BY(REWRITE_TAC[Ocbicby.MOD_5_EXPLICIT;arith `8 = 1*5 + 3`;arith `9 = 1*5 + 4`;MOD_MULT_ADD]);
  INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY ` generic (IMAGE v (:num)) (IMAGE (\i. {v i, v (SUC i)}) (:num)) /\ convex_local_fan (IMAGE v (:num),  IMAGE (\i. {v i, v (SUC i)}) (:num),  IMAGE (\i. v i,v (SUC i)) (:num))` (C SUBGOAL_THEN ASSUME_TAC);
    CONJ2_TAC;
      FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[LET_THM;Appendix.BBs_v39];
      BY(MESON_TAC[arith `~(5 <= 3)`]);
    BY(FIRST_X_ASSUM_ST `scs_generic` MP_TAC THEN MESON_TAC[Appendix.scs_generic]);
  FIRST_X_ASSUM MP_TAC THEN BURY_MP_TAC;
  COMMENT "first addition";
  SUBCONJ_TAC;
    INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`3`;`4`];
    ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 4 = 7 /\ 3 + 3  = 6 /\ 3 <= 5 /\ 0 < 3 /\ 3 < 4 /\ 4 < 5`];
    DISCH_THEN SUBST1_TAC;
    INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`2`;`3`];
    ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 3 = 6 /\ 3 + 2  = 5 /\ 3 <= 5 /\ 0 < 2 /\ 2 < 3 /\ 3 < 5`];
    DISCH_THEN SUBST1_TAC;
    BY(REAL_ARITH_TAC);
  DISCH_TAC;
  COMMENT "second addition";
  SUBCONJ_TAC;
    INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
    NUM_REDUCE_TAC;
    BY(ASM_REWRITE_TAC[LET_THM]);
  COMMENT "third addition";
  INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
  NUM_REDUCE_TAC;
  ASM_REWRITE_TAC[LET_THM];
  DISCH_TAC;
  DISCH_TAC;
  SUBCONJ_TAC;
    INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`1`;`2`;`4`];
    NUM_REDUCE_TAC;
    BY(ASM_REWRITE_TAC[LET_THM]);
  DISCH_TAC;
  TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i = j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[]);
  TYPIFY `!t. f (v 1) t = v 1 /\ f (v 2) t = v 2 /\ f (v 3) t = v 3` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN NUM_REDUCE_TAC);
  COMMENT "colinearity";
  TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0,v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT GEN_TAC THEN DISCH_TAC;
    MATCH_MP_TAC Zlzthic.PROPERTIES_GENERIC_LOCAL_FAN_ALT;
    GEXISTL_TAC [`IMAGE v (:num)`;`IMAGE (\i. {v i, v (SUC i)}) (:num)`;`IMAGE (\i. (v i, v (SUC i))) (:num)`];
    ASM_REWRITE_TAC[IN_IMAGE;IN_UNIV];
    CONJ_TAC;
      MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
      BY(ASM_REWRITE_TAC[]);
    BY(MESON_TAC[]);
  COMMENT "deform collinear";
  TYPIFY `!i j. ~collinear {vec 0,v i,v j} ==> (?e1. &0 < e1 /\ (!t. abs t < e1 ==> ~collinear {vec 0, f (v i) t, f (v j) t}))` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC (GEN_ALL Local_lemmas1.CONTINUOUS_PRESERVE_COLLINEAR) [`&0`;`(vec 0):real^3`;`f (v i)`;`f (v j)`];
    ANTS_TAC;
      FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation;arith `abs(&0 - x) = abs x`];
      REWRITE_TAC[IN_IMAGE;IN_UNIV];
      BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
    BY(REWRITE_TAC[arith `abs(&0 - r') = abs r'`]);
  TYPIFY `!i. azim (vec 0) (v i) (v (i+1)) (v(i+4)) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[arith `i+1 = SUC i`;arith `4 = 5 - 1`];
    GEN_TAC;
    MATCH_MP_TAC (REWRITE_RULE[LET_THM] Terminal.convex_local_fan_azim_le_pi);
    ASM_REWRITE_TAC[arith `3 <= 5`];
    FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM];
    BY(DISCH_THEN (unlist REWRITE_TAC));
  COMMENT "merge e";
  TYPIFY_GOAL_THEN `(?e1. &0 < e1 /\       (!t. abs t < e1            ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) =                azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) +                azim (vec 0) (v 3) (f (v 0) t) (v 1) +                azim (vec 0) (v 3) (v 1) (v 2) )) /\(?e1. &0 < e1 /\       (!t. abs t < e1            ==>                azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) =                azim (vec 0) (f (v 0) t) (v 1) (v 3) +                azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) )) /\ (?e1. &0 < e1 /\       (!t. abs t < e1            ==>                 azim (vec 0) (v 1) (v 2) (f (v 0) t) =                azim (vec 0) (v 1) (v 2) (v 3) +                azim (vec 0) (v 1) (v 3) (f (v 0) t))) /\ (?e1. &0 < e1 /\       (!t. abs t < e1            ==> &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\                azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi)) ==> (?e1. &0 < e1 /\       (!t. abs t < e1            ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) =                azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) +                azim (vec 0) (v 3) (f (v 0) t) (v 1) +                azim (vec 0) (v 3) (v 1) (v 2) /\                azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) =                azim (vec 0) (f (v 0) t) (v 1) (v 3) +                azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) /\                azim (vec 0) (v 1) (v 2) (f (v 0) t) =                azim (vec 0) (v 1) (v 2) (v 3) +                azim (vec 0) (v 1) (v 3) (f (v 0) t) /\                &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\                azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi))` (GMATCH_SIMP_TAC);
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC Cuxvzoz.epsilon_quad [`e1''`;`e1'''`;`e1''''`;`e1'''''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e''''` EXISTS_TAC;
    ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC THEN REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[];
      BY(ASM_MESON_TAC[]);
    BY(ASM_MESON_TAC[]);
  REWRITE_TAC[GSYM CONJ_ASSOC];
  COMMENT "azim bounds";
  TYPIFY `azim (vec 0) (v 0) (v 1) (v 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 4) < pi` MP_TAC;
    ASM_REWRITE_TAC[];
    MATCH_MP_TAC (arith `&0 <= y ==> (x + y < pi ==> x < pi)`);
    BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
  TYPIFY `~coplanar {vec 0,v 0,v 1,v 3}` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
    BY(REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 3)` MP_TAC) THEN REAL_ARITH_TAC);
  TYPIFY `&0 < azim (vec 0) (v 3) (v 0) (v 1) /\  &0 < azim (vec 0) (v 1) (v 3) (v 0)` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[Zlzthic.azim_pos_iff_nz];
    FIRST_X_ASSUM_ST `coplanar` MP_TAC;
    BY(MESON_TAC[Local_lemmas1.AZIM_COND_FOR_COPLANAR;SET_RULE `{a,b,c,d} = {a,d,b,c}`;SET_RULE `{a,b,c,d}={a,c,d,b}`]);
  INTRO_TAC Cuxvzoz.WNWSHJT_ALT [`v 3`;`v 0`;`v 1`;`f`;`-- e`;`e`;`pi - azim (vec 0) (v 0) (v 3) (v 4)`];
  ANTS_TAC;
    ASM_REWRITE_TAC[arith `a < pi - b <=> a + b < pi`];
    CONJ_TAC;
      MATCH_MP_TAC Zlzthic.deformation_subset;
      TYPIFY `IMAGE v (:num)` EXISTS_TAC;
      ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_UNIV];
      BY(MESON_TAC[FUN_IN_IMAGE;IN_UNIV]);
    REWRITE_TAC[CONJ_ASSOC];
    CONJ_TAC;
      FIRST_X_ASSUM_ST `coplanar` MP_TAC;
      BY(MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan;SET_RULE `{a,b,c} = {a,c,b}`]);
    BY(REPEAT (FIRST_X_ASSUM_ST `x < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Cuxvzoz.WNWSHJT_ALT [`v 0`;`v 1`;`v 3`;`f`;`-- e`;`e`;`pi - azim (vec 0) (v 1) (v 2) (v 3)`];
  ANTS_TAC;
    ASM_REWRITE_TAC[arith `a < pi - b <=> a + b < pi`];
    CONJ_TAC;
      MATCH_MP_TAC Zlzthic.deformation_subset;
      TYPIFY `IMAGE v (:num)` EXISTS_TAC;
      ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_UNIV];
      BY(MESON_TAC[FUN_IN_IMAGE;IN_UNIV]);
    REWRITE_TAC[CONJ_ASSOC];
    CONJ_TAC;
      FIRST_X_ASSUM_ST `coplanar` MP_TAC;
      BY(MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan;SET_RULE `{a,b,c} = {a,c,b}`]);
    BY(REPEAT (FIRST_X_ASSUM_ST `x < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "azim additivity";
  TYPIFY `?e3. &0 < e3 /\ (!t. abs t < e3 ==> ~collinear {vec 0,f (v 0) t,f (v 4) t} /\ ~collinear {vec 0,f (v 0) t,f (v 3) t} /\ ~collinear {vec 0,f (v 0) t,f (v 1) t} /\ ~collinear {vec 0,f (v 4) t,f (v 3) t})` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`4`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
    FIRST_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`3`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
    FIRST_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`1`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
    FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`4`;`3`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
    INTRO_TAC Cuxvzoz.epsilon_quad [`e1''`;`e1'''`;`e1''''`;`e1'''''`] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
    TYPIFY `e''''` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
    BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);
  FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
  SUBCONJ_TAC;
    INTRO_TAC Cuxvzoz.epsilon_triple [`e1`;`e1'`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e'''` EXISTS_TAC;
    ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC Cuxvzoz.azim_dominated_split [`(vec 0):real^3`;`v 3`;`v 4`;`v 1`;`v 2`;`(vec 0):real^3`;`v 3`;`f (v 4) t`;`v 1`;`v 2`];
    INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`3`;`4`];
    ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 4 = 7 /\ 3 + 3  = 6 /\ 3 <= 5 /\ 0 < 3 /\ 3 < 4 /\ 4 < 5`];
    DISCH_THEN (SUBST1_TAC o GSYM) THEN ASM_REWRITE_TAC[arith `x <= x`];
    INTRO_TAC Cuxvzoz.azim_dominated_split [`(vec 0):real^3`;`v 3`;`v 4`;`v 0`;`v 1`;`(vec 0):real^3`;`v 3`;`f (v 4) t`;`f (v 0) t`;`v 1`];
    ASM_REWRITE_TAC[arith `x <= x`];
    INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`2`;`3`];
    NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[LET_THM];
    ASM_REWRITE_TAC[];
    ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN ASM_REWRITE_TAC[];
    TYPIFY_GOAL_THEN `~collinear {vec 0, v 1, v 3} /\ ~collinear {vec 0, v 1, v 3} /\ ~collinear {vec 0, v 2, v 3}` (unlist REWRITE_TAC);
      BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
    BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  (DISCH_TAC);
  COMMENT "azim 0 additive";
  FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
  SUBCONJ_TAC;
    INTRO_TAC Cuxvzoz.epsilon_triple [`e'`;`e1'`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e''''` EXISTS_TAC;
    ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC Fan.sum3_azim_fan;
    ASM_REWRITE_TAC[];
    BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "azim 1 additive";
  SUBCONJ_TAC;
    INTRO_TAC Cuxvzoz.epsilon_pair [`e''`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e'''` EXISTS_TAC;
    ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC Fan.sum3_azim_fan;
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);
    ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
    ASM_REWRITE_TAC[];
    BY(CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "pi bounds";
  CONJ_TAC;
    TYPIFY `e'` EXISTS_TAC;
    CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
    TYPIFY ` &0 < azim (vec 0) (f (v 0) t) (f (v 1) t) (f (v 3) t) /\              azim (vec 0) (f (v 0) t) (f (v 1) t) (f (v 3) t) <              pi - azim (vec 0) (v 0) (v 3) (v 4)` ENOUGH_TO_SHOW_TAC;
      ASM_REWRITE_TAC[];
      MATCH_MP_TAC (arith `&0 <= b ==> (&0 < a /\ a < pi - b ==> &0 < a /\ a < pi)`);
      BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  MATCH_MP_TAC Oxl_def.periodic_numseg;
  TYPIFY `5` EXISTS_TAC;
  REWRITE_TAC[arith `~(5 = 0)`];
  CONJ_TAC;
    FIRST_X_ASSUM_ST `periodic` MP_TAC;
    REWRITE_TAC[Oxl_def.periodic];
    REWRITE_TAC[arith `(i+5)+j = (i+j)+5`];
    BY(DISCH_THEN (unlist REWRITE_TAC));
  REWRITE_TAC[IN_NUMSEG;arith `(0 <= i /\ i <= 5-1) <=> (i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4)`];
  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC;
          EXISTS_TAC `&1` THEN REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 4) < pi` MP_TAC);
          BY(MESON_TAC[arith `&0 < &1`;arith `x < pi ==> ~(x=pi)`]);
        REPEAT (FIRST_X_ASSUM_ST `+` kill);
        ASM_REWRITE_TAC[] THEN EXISTS_TAC `&1` THEN REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 1) (v 2) (v 0) < pi` MP_TAC);
        BY(MESON_TAC[arith `&0 < &1`;arith `x < pi ==> ~(x=pi)`]);
      BY(ASM_REWRITE_TAC[] THEN EXISTS_TAC `&1` THEN MESON_TAC[arith `&0 < &1`;arith `x <= x`]);
    INTRO_TAC Cuxvzoz.epsilon_triple [`e1''`;`e1'`;`e1`] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
    TYPIFY `e'''` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
    REPLICATE_TAC 3(FIRST_X_ASSUM (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC);
    REPEAT (FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `a = pi` (SUBST1_TAC o GSYM);
    ASM_REWRITE_TAC[];
    BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
  TYPIFY `e1'` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  REPEAT (FIRST_X_ASSUM_ST `4` (C INTRO_TAC [`t`]));
  ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)
*)

let azim5_reduction = 
prove_by_refinement(
 `!s f v e.
     is_scs_v39 s /\
     scs_k_v39 s = 5 /\
     BBs_v39 s v /\
     scs_generic v /\
     deformation f (IMAGE v (:num)) (--e,e) /\
     (!w t. ~(w = v 4) /\ ~(w = v 0) ==> f w t = w) /\
     azim (vec 0) (v 0) (v 1) (v 4) < pi /\
     azim (vec 0) (v 1) (v 2) (v 0) < pi /\
     &0 < azim (vec 0) (v 0) (v 1) (v 3) /\
     (?e1. &0 < e1 /\
           (!t. abs t < e1
                ==> azim (vec 0) (v 3) (f (v 0) t) (v 1) <=
                    azim (vec 0) (v 3) (v 0) (v 1))) /\
     (?e1. &0 < e1 /\ 
	(!t. abs t < e1
          ==> dist (v 3,f (v 4) t) = dist (v 3,v 4) /\
              dist (f (v 0) t,f (v 4) t) = dist (v 0,v 4) /\
              norm (f (v 4) t) = norm (v 4) /\
              dist (f (v 0) t,v 3) = dist (v 0,v 3) /\
              dist (f (v 0) t,v 1) = dist (v 0,v 1) - abs t /\
              norm (f (v 0) t) = norm (v 0) /\
	    (coplanar {vec 0, v 3, v 4, v 0}
                                 ==> coplanar {vec 0, v 3, f (v 4) t, f (v 0) t})))
     ==> azim (vec 0) (v 3) (v 4) (v 2) =
         azim (vec 0) (v 3) (v 4) (v 0) +
         azim (vec 0) (v 3) (v 0) (v 1) +
         azim (vec 0) (v 3) (v 1) (v 2) /\
         azim (vec 0) (v 0) (v 1) (v 4) =
         azim (vec 0) (v 0) (v 1) (v 3) + azim (vec 0) (v 0) (v 3) (v 4) /\
         azim (vec 0) (v 1) (v 2) (v 0) =
         azim (vec 0) (v 1) (v 2) (v 3) + azim (vec 0) (v 1) (v 3) (v 0) /\
         (?e1. &0 < e1 /\
               (!t. abs t < e1
                    ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) =
                        azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) +
                        azim (vec 0) (v 3) (f (v 0) t) (v 1) +
                        azim (vec 0) (v 3) (v 1) (v 2) /\
                        azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) =
                        azim (vec 0) (f (v 0) t) (v 1) (v 3) +
                        azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) /\
                        azim (vec 0) (v 1) (v 2) (f (v 0) t) =
                        azim (vec 0) (v 1) (v 2) (v 3) +
                        azim (vec 0) (v 1) (v 3) (f (v 0) t) /\
		        &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\
		        azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi)) /\
         (!i. ?e0. &0 < e0 /\
                   (azim (vec 0) (v i) (v (i + 1)) (v (i + 4)) = pi
                    ==> (!t. abs t < e0
                             ==> azim (vec 0) (f (v i) t) (f (v (i + 1)) t)
                                 (f (v (i + 4)) t) <=
                                 pi))) /\
         (?e1. &0 < e1 /\
           (!t. abs t < e1
                ==> azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) =
                    azim (vec 0) (v 3) (v 4) (v 0) /\
                    azim (vec 0) (f (v 4) t) (f (v 0) t) (v 3) =
                    azim (vec 0) (v 4) (v 0) (v 3) /\
                    azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) =
                    azim (vec 0) (v 0) (v 3) (v 4)))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  ASSUME_TAC (arith `~(0 = 5)`);
  TYPIFY `!i. i MOD 5 < 5` (C SUBGOAL_THEN ASSUME_TAC);
    BY((FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[DIVISION]);
  TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
  TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
    BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
  TYPIFY `v 5 = v 0 /\ v 6 = v 1 /\ v 7 = v 2 /\ v 8 = v 3 /\ v 9  = v 4` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
    BY(REWRITE_TAC[Ocbicby.MOD_5_EXPLICIT;arith `8 = 1*5 + 3`;arith `9 = 1*5 + 4`;MOD_MULT_ADD]);
  INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY ` generic (IMAGE v (:num)) (IMAGE (\i. {v i, v (SUC i)}) (:num)) /\ convex_local_fan (IMAGE v (:num),  IMAGE (\i. {v i, v (SUC i)}) (:num),  IMAGE (\i. v i,v (SUC i)) (:num))` (C SUBGOAL_THEN ASSUME_TAC);
    CONJ2_TAC;
      FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[LET_THM;Appendix.BBs_v39];
      BY(MESON_TAC[arith `~(5 <= 3)`]);
    BY(FIRST_X_ASSUM_ST `scs_generic` MP_TAC THEN MESON_TAC[Appendix.scs_generic]);
  FIRST_X_ASSUM MP_TAC THEN BURY_MP_TAC;
  COMMENT "first addition";
  SUBCONJ_TAC;
    INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`3`;`4`];
    ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 4 = 7 /\ 3 + 3  = 6 /\ 3 <= 5 /\ 0 < 3 /\ 3 < 4 /\ 4 < 5`];
    DISCH_THEN SUBST1_TAC;
    INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`2`;`3`];
    ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 3 = 6 /\ 3 + 2  = 5 /\ 3 <= 5 /\ 0 < 2 /\ 2 < 3 /\ 3 < 5`];
    DISCH_THEN SUBST1_TAC;
    BY(REAL_ARITH_TAC);
  DISCH_TAC;
  COMMENT "second addition";
  SUBCONJ_TAC;
    INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
    NUM_REDUCE_TAC;
    BY(ASM_REWRITE_TAC[LET_THM]);
  COMMENT "third addition";
  INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
  NUM_REDUCE_TAC;
  ASM_REWRITE_TAC[LET_THM];
  DISCH_TAC;
  DISCH_TAC;
  SUBCONJ_TAC;
    INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`1`;`2`;`4`];
    NUM_REDUCE_TAC;
    BY(ASM_REWRITE_TAC[LET_THM]);
  DISCH_TAC;
  TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i = j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[]);
  TYPIFY `!t. f (v 1) t = v 1 /\ f (v 2) t = v 2 /\ f (v 3) t = v 3` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN NUM_REDUCE_TAC);
  COMMENT "colinearity";
  TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0,v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT GEN_TAC THEN DISCH_TAC;
    MATCH_MP_TAC Zlzthic.PROPERTIES_GENERIC_LOCAL_FAN_ALT;
    GEXISTL_TAC [`IMAGE v (:num)`;`IMAGE (\i. {v i, v (SUC i)}) (:num)`;`IMAGE (\i. (v i, v (SUC i))) (:num)`];
    ASM_REWRITE_TAC[IN_IMAGE;IN_UNIV];
    CONJ_TAC;
      MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
      BY(ASM_REWRITE_TAC[]);
    BY(MESON_TAC[]);
  COMMENT "deform collinear";
  TYPIFY `!i j. ~collinear {vec 0,v i,v j} ==> (?e1. &0 < e1 /\ (!t. abs t < e1 ==> ~collinear {vec 0, f (v i) t, f (v j) t}))` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC (GEN_ALL Local_lemmas1.CONTINUOUS_PRESERVE_COLLINEAR) [`&0`;`(vec 0):real^3`;`f (v i)`;`f (v j)`];
    ANTS_TAC;
      FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation;arith `abs(&0 - x) = abs x`];
      REWRITE_TAC[IN_IMAGE;IN_UNIV];
      BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
    BY(REWRITE_TAC[arith `abs(&0 - r') = abs r'`]);
  TYPIFY `!i. azim (vec 0) (v i) (v (i+1)) (v(i+4)) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[arith `i+1 = SUC i`;arith `4 = 5 - 1`];
    GEN_TAC;
    MATCH_MP_TAC (REWRITE_RULE[LET_THM] Terminal.convex_local_fan_azim_le_pi);
    ASM_REWRITE_TAC[arith `3 <= 5`];
    FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM];
    BY(DISCH_THEN (unlist REWRITE_TAC));
  COMMENT "merge e";
  TYPIFY_GOAL_THEN `(?e1. &0 < e1 /\       (!t. abs t < e1            ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) =                azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) +                azim (vec 0) (v 3) (f (v 0) t) (v 1) +                azim (vec 0) (v 3) (v 1) (v 2) )) /\(?e1. &0 < e1 /\       (!t. abs t < e1            ==>                azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) =                azim (vec 0) (f (v 0) t) (v 1) (v 3) +                azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) )) /\ (?e1. &0 < e1 /\       (!t. abs t < e1            ==>                 azim (vec 0) (v 1) (v 2) (f (v 0) t) =                azim (vec 0) (v 1) (v 2) (v 3) +                azim (vec 0) (v 1) (v 3) (f (v 0) t))) /\ (?e1. &0 < e1 /\       (!t. abs t < e1            ==> &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\                azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi)) ==> (?e1. &0 < e1 /\       (!t. abs t < e1            ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) =                azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) +                azim (vec 0) (v 3) (f (v 0) t) (v 1) +                azim (vec 0) (v 3) (v 1) (v 2) /\                azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) =                azim (vec 0) (f (v 0) t) (v 1) (v 3) +                azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) /\                azim (vec 0) (v 1) (v 2) (f (v 0) t) =                azim (vec 0) (v 1) (v 2) (v 3) +                azim (vec 0) (v 1) (v 3) (f (v 0) t) /\                &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\                azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi))` (GMATCH_SIMP_TAC);
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC Cuxvzoz.epsilon_quad [`e1''`;`e1'''`;`e1''''`;`e1'''''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e''''` EXISTS_TAC;
    ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC THEN REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[];
      BY(ASM_MESON_TAC[]);
    BY(ASM_MESON_TAC[]);
  REWRITE_TAC[GSYM CONJ_ASSOC];
  COMMENT "azim bounds";
  TYPIFY `azim (vec 0) (v 0) (v 1) (v 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 4) < pi` MP_TAC;
    ASM_REWRITE_TAC[];
    MATCH_MP_TAC (arith `&0 <= y ==> (x + y < pi ==> x < pi)`);
    BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
  TYPIFY `~coplanar {vec 0,v 0,v 1,v 3}` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
    BY(REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 3)` MP_TAC) THEN REAL_ARITH_TAC);
  TYPIFY `&0 < azim (vec 0) (v 3) (v 0) (v 1) /\  &0 < azim (vec 0) (v 1) (v 3) (v 0)` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[Zlzthic.azim_pos_iff_nz];
    FIRST_X_ASSUM_ST `coplanar` MP_TAC;
    BY(MESON_TAC[Local_lemmas1.AZIM_COND_FOR_COPLANAR;SET_RULE `{a,b,c,d} = {a,d,b,c}`;SET_RULE `{a,b,c,d}={a,c,d,b}`]);
  INTRO_TAC Cuxvzoz.WNWSHJT_ALT [`v 3`;`v 0`;`v 1`;`f`;`-- e`;`e`;`pi - azim (vec 0) (v 0) (v 3) (v 4)`];
  ANTS_TAC;
    ASM_REWRITE_TAC[arith `a < pi - b <=> a + b < pi`];
    CONJ_TAC;
      MATCH_MP_TAC Zlzthic.deformation_subset;
      TYPIFY `IMAGE v (:num)` EXISTS_TAC;
      ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_UNIV];
      BY(MESON_TAC[FUN_IN_IMAGE;IN_UNIV]);
    REWRITE_TAC[CONJ_ASSOC];
    CONJ_TAC;
      FIRST_X_ASSUM_ST `coplanar` MP_TAC;
      BY(MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan;SET_RULE `{a,b,c} = {a,c,b}`]);
    BY(REPEAT (FIRST_X_ASSUM_ST `x < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Cuxvzoz.WNWSHJT_ALT [`v 0`;`v 1`;`v 3`;`f`;`-- e`;`e`;`pi - azim (vec 0) (v 1) (v 2) (v 3)`];
  ANTS_TAC;
    ASM_REWRITE_TAC[arith `a < pi - b <=> a + b < pi`];
    CONJ_TAC;
      MATCH_MP_TAC Zlzthic.deformation_subset;
      TYPIFY `IMAGE v (:num)` EXISTS_TAC;
      ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_UNIV];
      BY(MESON_TAC[FUN_IN_IMAGE;IN_UNIV]);
    REWRITE_TAC[CONJ_ASSOC];
    CONJ_TAC;
      FIRST_X_ASSUM_ST `coplanar` MP_TAC;
      BY(MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan;SET_RULE `{a,b,c} = {a,c,b}`]);
    BY(REPEAT (FIRST_X_ASSUM_ST `x < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "034 triangle";
  TYPIFY `?e3. &0 < e3 /\ (!t. abs t < e3 ==> ~collinear {vec 0,f (v 0) t,f (v 4) t} /\ ~collinear {vec 0,f (v 0) t,f (v 3) t} /\ ~collinear {vec 0,f (v 0) t,f (v 1) t} /\ ~collinear {vec 0,f (v 4) t,f (v 3) t})` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`4`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
    FIRST_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`3`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
    FIRST_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`1`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
    FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`4`;`3`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
    INTRO_TAC Cuxvzoz.epsilon_quad [`e1''`;`e1'''`;`e1''''`;`e1'''''`] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
    TYPIFY `e''''` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
    BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);
  FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
  TYPIFY `!i. f (v i) (&0) = v i` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
    REPEAT WEAKER_STRIP_TAC;
    BY(FIRST_X_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC FUN_IN_IMAGE THEN REWRITE_TAC[IN_UNIV]);
  REWRITE_TAC[CONJ_ASSOC] THEN SUBCONJ2_TAC;
    TYPIFY `?e2. &0 < e2 /\ (!t. abs t < e2 ==> azim (vec 0) (f (v 4) t) (f (v 0) t) (v 3) <= pi)` ASM_CASES_TAC;
      FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
      INTRO_TAC Cuxvzoz.epsilon_triple [`e1'`;`e3`;`e2`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
      TYPIFY `e'''` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
      REPLICATE_TAC 3 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
      REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
      TYPIFY `azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) <= pi /\ azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) <= pi /\ azim (vec 0) (v 0) (v 3) (v 4) <= pi /\ azim (vec 0) (v 3) (v 4) (v 0) <= pi /\ azim (vec 0) (v 4) (v 0) (v 3) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
        FIRST_X_ASSUM MP_TAC THEN (FIRST_X_ASSUM_ST `x <= pi` (C INTRO_TAC [`4`]));
        NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[];
        BY(MESON_TAC[Xivphks.FSQKWKK]);
      FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
      REPEAT (FIRST_X_ASSUM_ST `a <= pi` (ASSUME_TAC o (MATCH_MP (REWRITE_RULE[TAUT `(a /\ b /\ c ==> d) <=> (c ==> (a /\ b ==> d))`] azim_dih_y))));
      REPLICATE_TAC 6 (POP_ASSUM GMATCH_SIMP_TAC);
      ASM_REWRITE_TAC[];
      ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN ASM_REWRITE_TAC[];
      TYPIFY_GOAL_THEN `(~collinear {vec 0, v 0, v 4} /\ ~collinear {vec 0, v 3, v 4}) /\ (~collinear {vec 0, v 4, v 3} /\ ~collinear {vec 0, v 0, v 3}) /\ (~collinear {vec 0, v 3, v 0} /\ ~collinear {vec 0, v 4, v 0})` (unlist REWRITE_TAC);
        BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
      ASM_REWRITE_TAC[DIST_SYM];
      BY(REPEAT (FIRST_X_ASSUM_ST `dist` MP_TAC) THEN REWRITE_TAC[DIST_SYM;DIST_0] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[]);
    PROOF_BY_CONTR_TAC;
    FIRST_X_ASSUM kill;
    FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[];
    COMMENT "second half of assumption. All angles 034 <=pi";
    TYPIFY `coplanar {vec 0, v 3, v 4, v 0}` ASM_CASES_TAC;
      TYPIFY `e1'` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM_ST `coplanar` (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM MP_TAC;
      TYPIFY `{vec 0, v 3, f (v 4) t, f (v 0) t} = {vec 0,  f (v 4) t, f (v 0) t, v 3}` (C SUBGOAL_THEN SUBST1_TAC);
        BY(SET_TAC[]);
      REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
      BY(MP_TAC PI_POS THEN REAL_ARITH_TAC);
    POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {a,c,d,b}`] THEN REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR;DE_MORGAN_THM] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `&0 < azim (vec 0) (v 4) (v 0) (v 3) /\ azim (vec 0) (v 4) (v 0) (v 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
      REWRITE_TAC[arith `&0 < x <=> &0 <= x /\ ~(x = &0) `;arith `x < pi <=> x <= pi /\ ~(x = pi)`];
      REWRITE_TAC[Counting_spheres.AZIM_NN];
      ASM_REWRITE_TAC[];
      FIRST_X_ASSUM_ST `a <= pi` (C INTRO_TAC [`4`]) THEN NUM_REDUCE_TAC;
      BY(ASM_REWRITE_TAC[]);
    TYPIFY `&0 < e` (C SUBGOAL_THEN ASSUME_TAC);
      FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation;IN_REAL_INTERVAL];
      BY(MESON_TAC[]);
    INTRO_TAC Cuxvzoz.epsilon_pair [`e3`;`e`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC Zlzthic.WNWSHJT [`v 3`;`v 4`;`v 0`;`f`;`-- e'''`;`e'''`] THEN ASM_REWRITE_TAC[];
    ANTS_TAC;
      TYPIFY_GOAL_THEN `~collinear {vec 0, v 4, v 0} /\ ~collinear {vec 0, v 4, v 3}` (unlist REWRITE_TAC);
        BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
      MATCH_MP_TAC Cuxvzoz.deformation_restrict;
      TYPIFY `e` EXISTS_TAC THEN ASM_REWRITE_TAC[];
      MATCH_MP_TAC Zlzthic.deformation_subset;
      TYPIFY `(IMAGE v (:num))` EXISTS_TAC;
      ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
      BY(GEN_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC FUN_IN_IMAGE THEN REWRITE_TAC[IN_UNIV]);
    BY(MESON_TAC[arith `x < pi ==> x <= pi`]);
  (REPEAT WEAKER_STRIP_TAC THEN REWRITE_TAC[GSYM CONJ_ASSOC]);
  COMMENT "azim additivity";
  SUBCONJ_TAC;
    INTRO_TAC Cuxvzoz.epsilon_triple [`e1`;`e1''`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e'''` EXISTS_TAC;
    ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC Cuxvzoz.azim_dominated_split [`(vec 0):real^3`;`v 3`;`v 4`;`v 1`;`v 2`;`(vec 0):real^3`;`v 3`;`f (v 4) t`;`v 1`;`v 2`];
    INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`3`;`4`];
    ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 4 = 7 /\ 3 + 3  = 6 /\ 3 <= 5 /\ 0 < 3 /\ 3 < 4 /\ 4 < 5`];
    DISCH_THEN (SUBST1_TAC o GSYM) THEN ASM_REWRITE_TAC[arith `x <= x`];
    INTRO_TAC Cuxvzoz.azim_dominated_split [`(vec 0):real^3`;`v 3`;`v 4`;`v 0`;`v 1`;`(vec 0):real^3`;`v 3`;`f (v 4) t`;`f (v 0) t`;`v 1`];
    ASM_REWRITE_TAC[arith `x <= x`];
    INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`2`;`3`];
    NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[LET_THM];
    ASM_REWRITE_TAC[];
    ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN ASM_REWRITE_TAC[];
    TYPIFY_GOAL_THEN `~collinear {vec 0, v 1, v 3} /\ ~collinear {vec 0, v 1, v 3} /\ ~collinear {vec 0, v 2, v 3}` (unlist REWRITE_TAC);
      BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
    BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  COMMENT "azim 0 additive";
  REPEAT WEAKER_STRIP_TAC;
  SUBCONJ_TAC;
    INTRO_TAC Cuxvzoz.epsilon_triple [`e'`;`e1''`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e''''` EXISTS_TAC;
    ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC Fan.sum3_azim_fan;
    ASM_REWRITE_TAC[];
    BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "azim 1 additive";
  SUBCONJ_TAC;
    INTRO_TAC Cuxvzoz.epsilon_pair [`e''`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e'''` EXISTS_TAC;
    ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC Fan.sum3_azim_fan;
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);
    ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
    ASM_REWRITE_TAC[];
    BY(CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "pi bounds";
  CONJ_TAC;
    TYPIFY `e'` EXISTS_TAC;
    CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
    TYPIFY ` &0 < azim (vec 0) (f (v 0) t) (f (v 1) t) (f (v 3) t) /\              azim (vec 0) (f (v 0) t) (f (v 1) t) (f (v 3) t) <              pi - azim (vec 0) (v 0) (v 3) (v 4)` ENOUGH_TO_SHOW_TAC;
      ASM_REWRITE_TAC[];
      MATCH_MP_TAC (arith `&0 <= b ==> (&0 < a /\ a < pi - b ==> &0 < a /\ a < pi)`);
      BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  MATCH_MP_TAC Oxl_def.periodic_numseg;
  TYPIFY `5` EXISTS_TAC;
  REWRITE_TAC[arith `~(5 = 0)`];
  CONJ_TAC;
    FIRST_X_ASSUM_ST `periodic` MP_TAC;
    REWRITE_TAC[Oxl_def.periodic];
    REWRITE_TAC[arith `(i+5)+j = (i+j)+5`];
    BY(DISCH_THEN (unlist REWRITE_TAC));
  REWRITE_TAC[IN_NUMSEG;arith `(0 <= i /\ i <= 5-1) <=> (i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4)`];
  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC;
          EXISTS_TAC `&1` THEN REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 4) < pi` MP_TAC);
          BY(MESON_TAC[arith `&0 < &1`;arith `x < pi ==> ~(x=pi)`]);
        REPEAT (FIRST_X_ASSUM_ST `+` kill);
        ASM_REWRITE_TAC[] THEN EXISTS_TAC `&1` THEN REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 1) (v 2) (v 0) < pi` MP_TAC);
        BY(MESON_TAC[arith `&0 < &1`;arith `x < pi ==> ~(x=pi)`]);
      BY(ASM_REWRITE_TAC[] THEN EXISTS_TAC `&1` THEN MESON_TAC[arith `&0 < &1`;arith `x <= x`]);
    INTRO_TAC Cuxvzoz.epsilon_triple [`e1'''`;`e1''`;`e1`] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
    TYPIFY `e'''` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
    REPLICATE_TAC 3(FIRST_X_ASSUM (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC);
    REPEAT (FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `a = pi` (SUBST1_TAC o GSYM);
    ASM_REWRITE_TAC[];
    BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
  TYPIFY `e1''` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `azim a b c d = azim a' b' c' d'` (C INTRO_TAC [`t`]);
  BY(ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[arith `x <= x`])
  ]);;
  (* }}} *)

let L13_LEMMA = 
prove_by_refinement(
  `main_nonlinear_terminal_v11
 ==>
 (!V E FF s v. IMAGE (\i. v i,v (SUC i)) (:num) = FF
 /\ is_scs_v39 s
 /\ scs_k_v39 s = 5
 /\ scs_basic_v39 s
 /\ scs_generic v
 /\ BBs_v39 s v
 /\ IMAGE v (:num) = V
 /\ IMAGE (\i. {v i, v (SUC i)}) (:num) = E
 /\ ~coplanar {vec 0, v 1, v 2, v 0}
 ==> &0 < azim (vec 0) (v 0) (v 1) (v 3) )`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[arith `&0 < a <=> ~(a = &0) /\ (&0 <= a)`];
  REWRITE_TAC[Counting_spheres.AZIM_NN];
  DISCH_TAC;
  FIRST_X_ASSUM_ST `coplanar {vec 0,v 1 ,v 2,v 0}` MP_TAC;
  REWRITE_TAC[];
  INTRO_TAC EGHNAVX_SCS [`s`;`5`;`v`;`0`];
  ASM_REWRITE_TAC[LET_THM];
  NUM_REDUCE_TAC;
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM kill;
  FIRST_X_ASSUM (C INTRO_TAC [`3`;`2`]);
  NUM_REDUCE_TAC;
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[coplanar];
  GEXISTL_TAC [`(vec 0):real^3`;`v 0`;`v 1`];
  TYPIFY `{vec 0, v 0, v 1} SUBSET affine hull  {vec 0, v 0, v 1} /\  v 2 IN affine hull  {vec 0, v 0, v 1}` ENOUGH_TO_SHOW_TAC;
    BY(SET_TAC[]);
  REWRITE_TAC[HULL_SUBSET];
  INTRO_TAC AFF_GT_SUBSET_AFFINE_HULL [`{vec 0,v 0}`;`{v 1}`];
  TYPIFY `{vec 0, v 0} UNION {v 1} = {vec 0, v 0, v 1}` (C SUBGOAL_THEN SUBST1_TAC);
    BY(SET_TAC[]);
  BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[])
  ]);;
  (* }}} *)

let IUNBUIG = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> 
  (!s FF v.
  IMAGE (\i. (v i,v (SUC i))) (:num) = FF /\
  is_scs_v39 s /\
  scs_k_v39 s = 5 /\
  MMs_v39 s v /\
  scs_basic_v39 s /\
  scs_generic v /\
  (!i j. scs_diag 5 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4 * h0 < scs_b_v39 s i j) /\
  scs_a_v39 s 0 1 = &2 /\
  scs_b_v39 s 0 1 <= cstab /\
     interior_angle1 (vec 0) FF (v 0) < pi /\      interior_angle1 (vec 0) FF (v 1) < pi /\
  (!i. ~(i MOD 5 = 0)  ==> dist(v i,v (i+1)) = &2) /\
  xrr (norm (v 0)) (norm (v 3)) (dist(v 0,v 3)) <= #15.53 /\ 
  xrr (norm (v 1)) (norm (v 3)) (dist(v 1,v 3)) <= #15.53 ==>
  dist(v 0,v 1) = &2)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `BBprime2_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Appendix.scs_basic;Ayqjtmd.unadorned_MMs]);
  TYPIFY `BBprime_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Appendix.BBprime2_v39]);
  TYPIFY `BBs_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_MESON_TAC[Appendix.BBprime_v39]);
  INTRO_TAC Appendix.BBs_v39 [`s`;`v`];
  ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;Terminal.IMAGE_SUBSET_IN;IN_UNIV;arith `~(5 <= 3)`];
  REPEAT WEAKER_STRIP_TAC;
  TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
  TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
  TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    EXPAND_TAC "V";
    REWRITE_TAC[IN_IMAGE;IN_UNIV];
    BY(MESON_TAC[]);
  INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  TYPIFY `!i. interior_angle1 (vec 0) FF (v i) = azim (vec 0) (v i) (v (i+1)) (v (i+4))` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    EXPAND_TAC "FF";
    GMATCH_SIMP_TAC (REWRITE_RULE[LET_THM] (GSYM Ocbicby.INTERIOR_ANGLE1_AZIM));
    TYPIFY `s` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[IN;arith `5 - 1 = 4`;arith `3 < 5`;arith `SUC i = i+1`]);
  INTRO_TAC Ocbicby.LOCAL_FAN_AZIM_POS [`s`;`v`];
  ASM_REWRITE_TAC[LET_THM;IN;arith `5-1 = 4`;arith `SUC i = i+1`];
  DISCH_TAC;
  TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
    GEN_TAC;
    MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
    BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
  TYPIFY `v 5 = v 0 /\ v 6 = v 1 /\ v 7 = v 2 /\ v 8 = v 3 /\ v 9  = v 4` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
    BY(REWRITE_TAC[Ocbicby.MOD_5_EXPLICIT;arith `8 = 1*5 + 3`;arith `9 = 1*5 + 4`;MOD_MULT_ADD]);
  TYPIFY `~coplanar {vec 0, v 0,v 1,v 4} /\ ~coplanar {vec 0,v 1,v 2,v 0}` (C SUBGOAL_THEN ASSUME_TAC);
    ASM_REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
    BY(ASM_MESON_TAC[arith `x < pi ==> ~(x = pi)`;arith `&0 < a ==> ~(a = &0)`;arith `0+i=i`;arith `1+1=2 /\ 1+4=5`]);
  TYPIFY `generic V E` (C SUBGOAL_THEN ASSUME_TAC);
    BY(FIRST_X_ASSUM_ST `scs_generic` MP_TAC THEN ASM_REWRITE_TAC[Appendix.scs_generic]);
  INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
  NUM_REDUCE_TAC;
  ASM_REWRITE_TAC[LET_THM];
  DISCH_TAC;
  COMMENT "collinearity";
  TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0,v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT GEN_TAC THEN DISCH_TAC;
    MATCH_MP_TAC Zlzthic.PROPERTIES_GENERIC_LOCAL_FAN_ALT;
    GEXISTL_TAC [`IMAGE v (:num)`;`IMAGE (\i. {v i, v (SUC i)}) (:num)`;`IMAGE (\i. (v i, v (SUC i))) (:num)`];
    ASM_REWRITE_TAC[IN_IMAGE;IN_UNIV];
    BY(MESON_TAC[]);
  TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i = j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
  COMMENT "non coplanar 013 digression";
  INTRO_TAC (UNDISCH L13_LEMMA) [`V`;`E`;`FF`;`s`;`v`];
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  REPEAT (FIRST_X_ASSUM_ST `interior_angle1 a b c < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC;
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `azim (vec 0) (v 0) (v 1) (v 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `+` MP_TAC;
    MATCH_MP_TAC (arith `&0 <= a2 /\ a < pi   ==> (a = a1 + a2 ==> a1 < pi)`);
    REWRITE_TAC[Counting_spheres.AZIM_NN];
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `~coplanar {vec 0,v 0, v 1,v 3}` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
    BY(REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  COMMENT "introduce deformation";
  INTRO_TAC deform_pent_exists [`V`;`(\t. -- abs t)`;`v 3`;`v 4`;`v 0`;`v 1`;`&1`];
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  ANTS_TAC;
    REWRITE_TAC[arith `&0 < &1`;arith `--abs (&0) = &0`];
    CONJ_TAC;
      DISCH_TAC;
      INTRO_TAC coplanar_cross_reduction [`s`;`5`;`v`;`3`];
      NUM_REDUCE_TAC;
      BY(ASM_REWRITE_TAC[]);
    CONJ_TAC;
      FIRST_X_ASSUM MP_TAC;
      BY(MESON_TAC[SET_RULE `{a,b,c,d} = {a,d,b,c}`]);
    CONJ_TAC;
      BY(REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
    CONJ_TAC;
      INTRO_TAC (GEN_ALL Local_lemmas.CONVEX_LOFA_IMP_INANGLE_LE_PI) [`E`;`V`;`FF`;`v 4`];
      ASM_REWRITE_TAC[];
      NUM_REDUCE_TAC;
      BY(ASM_REWRITE_TAC[]);
    CONJ_TAC;
      INTRO_TAC Trigonometry.JBDNJJB [`v 0`;`v 1`;`v 3`];
      TYPIFY `v 0 dot (v 1 cross v 3) = ((v 0 cross v 1) dot v 3)` (C SUBGOAL_THEN SUBST1_TAC);
        BY(VEC3_TAC);
      REWRITE_TAC[arith `x > &0 <=> &0 < x`];
      ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
      REWRITE_TAC[Trigonometry2.re_eqvl];
      REPEAT WEAKER_STRIP_TAC;
      ASM_REWRITE_TAC[];
      GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
      BY(ASM_REWRITE_TAC[Cuxvzoz.sin_azim_pos]);
    GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
    REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
    REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC REAL_CONTINUOUS_NEG;
    BY(REWRITE_TAC[Cuxvzoz.real_continuous_abs]);
  REPEAT WEAKER_STRIP_TAC;
  (COMMENT "reduction lemmas");
  PROOF_BY_CONTR_TAC;
  TYPIFY `&2 < dist(v 0,v 1)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `scs_a_v39` (C INTRO_TAC [`0`;`1`]);
    BY(ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  FIRST_X_ASSUM_ST `~` MP_TAC THEN REWRITE_TAC[];
  TYPIFY `!i. f (v i) (&0) = v i` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
    BY(ASM_MESON_TAC[]);
  INTRO_TAC a5_assumption_reduction [`s`;`f`;`v`;`e'`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM_ST `scs_diag` (C INTRO_TAC [`i`;`j`]);
      BY(ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
    CONJ_TAC;
      TYPIFY `e'` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
      FIRST_X_ASSUM (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[DIST_SYM];
      BY(MESON_TAC[]);
    INTRO_TAC Cuxvzoz.continuous_nbd_pos [`\ t. dist(f (v 0) t,v 1) - &2`;`&0`];
    ASM_REWRITE_TAC[arith `abs (t' - &0) = abs t'`;arith `&0 < a - b <=> b < a`];
    ANTS_TAC;
      FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM_ST `atreal` (C INTRO_TAC [`v 0`;`&0`]);
      ASM_REWRITE_TAC[];
      DISCH_TAC;
      BY((REPEAT (REPEAT CONJ_TAC THEN (MATCH_MP_TAC REAL_CONTINUOUS_ADD ORELSE MATCH_MP_TAC Local_lemmas1.CON_ATREAL_REAL_CON ORELSE MATCH_MP_TAC Local_lemmas1.CON_ATREAL_REAL_CON2 ORELSE MATCH_MP_TAC REAL_CONTINUOUS_MUL ORELSE MATCH_MP_TAC REAL_CONTINUOUS_POW ORELSE MATCH_MP_TAC REAL_CONTINUOUS_SUB THEN ASM_REWRITE_TAC[REAL_CONTINUOUS_CONST;ETA_AX]))));
    BY(MESON_TAC[arith `x < y ==> x <= y`]);
  DISCH_TAC;
  (COMMENT "b5 reduction");
  INTRO_TAC b5_assumption_reduction [`s`;`f`;`v`;`e'`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    CONJ_TAC;
      BY(ASM_MESON_TAC[]);
    CONJ_TAC;
      TYPIFY `e'` EXISTS_TAC;
      FIRST_X_ASSUM_ST `norm` MP_TAC THEN ASM_REWRITE_TAC[DIST_SYM];
      BY(MESON_TAC[]);
    TYPIFY `e'` EXISTS_TAC;
    CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
    FIRST_X_ASSUM_ST `norm` (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[DIST_SYM];
    DISCH_THEN (unlist REWRITE_TAC);
    BY(REAL_ARITH_TAC);
  DISCH_TAC;
  COMMENT "deform collinear";
  TYPIFY `!t. f (v 1) t = v 1 /\ f (v 2) t = v 2 /\ f (v 3) t = v 3` (C SUBGOAL_THEN ASSUME_TAC);
    BY(GEN_TAC THEN REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN NUM_REDUCE_TAC);
  TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(v i = v j) ==> (?e. &0 < e /\ (!t. abs t < e==> ~collinear {vec 0, f (v i) t, f (v j) t}))` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC (GEN_ALL Local_lemmas1.CONTINUOUS_PRESERVE_COLLINEAR) [`&0`;`(vec 0):real^3`;`f (v i)`;`f (v j)`];
    REWRITE_TAC[arith `abs(&0 - r') = abs r'`] THEN DISCH_THEN MATCH_MP_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
    REPEAT WEAKER_STRIP_TAC;
    REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC;
      BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
    FIRST_X_ASSUM MATCH_MP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_MESON_TAC[]);
  TYPIFY `!i. azim (vec 0) (v i) (v (i+1)) (v(i+4)) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
    REWRITE_TAC[arith `i+1 = SUC i`;arith `4 = 5 - 1`];
    GEN_TAC;
    MATCH_MP_TAC (REWRITE_RULE[LET_THM] Terminal.convex_local_fan_azim_le_pi);
    ASM_REWRITE_TAC[arith `3 <= 5`];
    FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM];
    BY(ASM_REWRITE_TAC[]);
  COMMENT "coplanar";
  INTRO_TAC Zlzthic.NONPLANAR_OPEN [`(\ (t:real). (vec 0):real^3)`;`f (v 0)`;`\ (t:real). v 1`;`\ (t:real). v 3`;`&0`];
  ASM_REWRITE_TAC[CONTINUOUS_CONST];
  ANTS_TAC;
    FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation] THEN REPEAT WEAKER_STRIP_TAC;
    BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
  REWRITE_TAC[arith `abs (&0 - t') = abs t'`] THEN REPEAT WEAKER_STRIP_TAC;
  COMMENT "azim reduction";
  INTRO_TAC azim5_reduction [`s`;`f`;`v`;`e'`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    CONJ_TAC;
      BY(REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `a < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[]);
    CONJ2_TAC;
      TYPIFY `e'` EXISTS_TAC;
      BY(ASM_REWRITE_TAC[arith `x - abs t = x + --abs t`]);
    INTRO_TAC Zlzthic.WNWSHJT [`v 1`;`v 3`;`v 0`;`f`;`-- e'`;`e'`];
    ASM_REWRITE_TAC[];
    ANTS_TAC;
      CONJ_TAC;
        MATCH_MP_TAC Zlzthic.deformation_subset;
        TYPIFY `V` EXISTS_TAC;
        ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
        BY(EXPAND_TAC "V" THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC FUN_IN_IMAGE THEN REWRITE_TAC[IN_UNIV]);
      TYPIFY_GOAL_THEN `~collinear {vec 0, v 3, v 0} /\ ~collinear {vec 0, v 3, v 1}` (unlist REWRITE_TAC);
        BY(CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
      FIRST_X_ASSUM_ST `coplanar` kill;
      FIRST_X_ASSUM_ST `~coplanar s` MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {a,d,b,c}`] THEN REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
      REWRITE_TAC[arith `&0 < a <=> &0 <= a /\ ~(a = &0)`];
      REWRITE_TAC[Counting_spheres.AZIM_NN];
      REWRITE_TAC[arith `a < pi <=> a <= pi /\ ~(a = pi)`;DE_MORGAN_THM];
      DISCH_THEN (unlist REWRITE_TAC);
      REPLICATE_TAC 2(MATCH_MP_TAC Xivphks.FSQKWKK);
      FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`0`]) THEN NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[];
      MATCH_MP_TAC (arith `&0 <= a2 ==> (a1 + a2 <= pi ==> a1 <= pi)`);
      BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
    (REPEAT WEAKER_STRIP_TAC);
    INTRO_TAC Cuxvzoz.epsilon_triple [`e`;`e''`;`e'`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e''''` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    REPLICATE_TAC 3 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC azim_dih_y [`(vec 0):real^3`;`v 3`;`f (v 0) t`;`v 1`];
    INTRO_TAC azim_dih_y [`(vec 0):real^3`;`v 3`;`(v 0)`;`v 1`];
    DISCH_THEN GMATCH_SIMP_TAC;
    CONJ_TAC;
      FIRST_X_ASSUM_ST `x < pi` (C INTRO_TAC [`&0`]) THEN ASM_REWRITE_TAC[arith `abs(&0) = &0`];
      SIMP_TAC[arith `x < pi ==> x <= pi`];
      DISCH_TAC;
      BY(CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
    DISCH_THEN GMATCH_SIMP_TAC;
    CONJ_TAC;
      REWRITE_TAC[CONJ_ASSOC] THEN CONJ2_TAC;
        MATCH_MP_TAC (arith `x < pi ==> x <= pi`);
        BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
      CONJ_TAC;
        ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
        BY(FIRST_X_ASSUM_ST `coplanar` (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan]);
      BY(REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
    FIRST_X_ASSUM_ST `norm` (C INTRO_TAC [`t`]);
    ASM_REWRITE_TAC[DIST_SYM;DIST_0];
    REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[];
    MATCH_MP_TAC Ocbicby.dih_y_mono;
    FIRST_X_ASSUM_ST `~coplanar s` (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `~coplanar s` MP_TAC;
    REPEAT WEAKER_STRIP_TAC;
    REWRITE_TAC[arith `d + -- abs t <= d`];
    CONJ_TAC;
      REWRITE_TAC[NORM_POS_LT];
      POP_ASSUM (MP_TAC o (MATCH_MP Planarity.notcoplanar_disjoint));
      BY(MESON_TAC[]);
    CONJ_TAC;
      FIRST_X_ASSUM_ST `abs` (SUBST1_TAC o GSYM);
      REWRITE_TAC[GSYM DIST_NZ];
      POP_ASSUM (MP_TAC o (MATCH_MP Planarity.notcoplanar_disjoint));
      BY(MESON_TAC[]);
    CONJ_TAC;
      POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Oxlzlez.coplanar_delta_y;DIST_SYM;DIST_0];
      BY(MESON_TAC[Merge_ineq.delta_y_sym]);
    INTRO_TAC Terminal.DELTA_Y_POS_4POINTS [`(vec 0):real^3`;`v 3`;`v 0`;`v 1`];
    BY(REWRITE_TAC[DIST_0;DIST_SYM]);
  REPEAT WEAKER_STRIP_TAC;
  (COMMENT "end of azim reduction");
  COMMENT "deformation in BBs";
  INTRO_TAC Cuxvzoz.deformation_BBs_ALT [`s`;`5`;`f`;`v`;`e'`];
  NUM_REDUCE_TAC;
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    MATCH_MP_TAC Terminal.periodic_mod_reduce;
    TYPIFY `5` EXISTS_TAC THEN REWRITE_TAC[arith `~(5 = 0)`];
    CONJ_TAC;
      FIRST_X_ASSUM_ST `periodic` MP_TAC THEN REWRITE_TAC[Oxl_def.periodic];
      BY(MESON_TAC[]);
    REWRITE_TAC[arith `i < 5 <=> i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4`];
    REPEAT WEAKER_STRIP_TAC THEN (FIRST_X_ASSUM_ST `norm` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
    BY(FIRST_X_ASSUM_ST ` \/ ` MP_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  COMMENT "back to root, next tau";
  TYPIFY `!t. abs t < e'' ==>     sum {i | i < 5} (\i. rho_fun (norm (v i)) * azim (vec 0) (v i) (v (i + 1)) (v (i + 5 - 1))) <=    sum {i | i < 5} (\i. rho_fun (norm (f (v i) t)) * azim (vec 0) (f (v i) t) (f(v(i+1)) t) (f (v (i + 5 - 1)) t))` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC Cuxvzoz.MMs_minimize_tau_fun;
    TYPIFY `s` EXISTS_TAC;
    ASM_REWRITE_TAC[arith `3 < 5`];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(FIRST_X_ASSUM (unlist REWRITE_TAC));
  POP_ASSUM MP_TAC;
  TYPIFY `{i | i < 5} = 0..4` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC);
  REWRITE_TAC[SUM_NUMSEG4];
  NUM_REDUCE_TAC;
  DISCH_TAC;
  COMMENT "introduce nonlinear 684";
  TYPIFY `scs_diag 5 0 2 /\ scs_diag 5 0 3 /\ scs_diag 5 1 3 /\ scs_diag 5 1 4 /\ scs_diag 5 2 4` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
  INTRO_TAC (UNDISCH Ocbicby.LEMMA_6843920790) [`norm (v 3)`;`norm (v 0)`;`norm (v 1)`;`dist(v 0,v 1)`;`dist (v 1,v 3)`;`dist(v 0,v 3)`];
  ASM_REWRITE_TAC[];
  ANTS_TAC;
    ONCE_REWRITE_TAC[Ocbicby.xrr_sym];
    ASM_REWRITE_TAC[GSYM Sphere.cstab];
    TYPIFY_GOAL_THEN `(&2 <= norm (v 3) /\ norm (v 3) <= &2 * h0) /\ (&2 <= norm (v 0) /\ norm (v 0) <= &2 * h0) /\ (&2 <= norm (v 1) /\ norm (v 1) <= &2 * h0)` (unlist REWRITE_TAC);
      REWRITE_TAC[GSYM Fnjlbxs.in_ball_annulus];
      FIRST_X_ASSUM_ST `BBs_v39` kill THEN FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN EXPAND_TAC "V" THEN REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM_ST `ball_annulus` MP_TAC;
      REWRITE_TAC[SUBSET;IN_IMAGE;IN_UNIV];
      BY(MESON_TAC[]);
    REWRITE_TAC[ CONJ_ASSOC] THEN CONJ2_TAC;
      INTRO_TAC Oxlzlez.coplanar_delta_y [`(vec 0):real^3`;`v 3`;`v 0`;`v 1`];
      REWRITE_TAC[DIST_0;DIST_SYM] THEN DISCH_THEN (SUBST1_TAC o GSYM);
      BY(ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {a,c,d,b}`] THEN ASM_REWRITE_TAC[]);
    TYPIFY_GOAL_THEN `(&2 <= dist (v 0,v 1) /\ dist (v 0,v 1) <= cstab)` (unlist REWRITE_TAC);
      REPEAT (FIRST_X_ASSUM_ST `scs_a_v39` (C INTRO_TAC [`0`;`1`])) THEN FIRST_X_ASSUM_ST `scs_a_v39 s 0 1 = &2` MP_TAC THEN FIRST_X_ASSUM_ST `scs_b_v39 s 0 1 <= cstab` MP_TAC;
      BY(REAL_ARITH_TAC);
    CONJ_TAC;
      REPEAT (FIRST_X_ASSUM_ST `scs_a_v39` (C INTRO_TAC [`1`;`3`]) );
      BY(ASM_REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
    REPEAT (FIRST_X_ASSUM_ST `scs_a_v39` (C INTRO_TAC [`0`;`3`]) );
    BY(ASM_REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  PROOF_BY_CONTR_TAC;
  FIRST_X_ASSUM_ST `IN` MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;TAUT `~(a ==> b) <=> (a /\ ~b)`;arith `~(a < b) <=> b <= a`];
  TYPIFY `?e2. &0 < e2 /\ (!t. abs t < e2 ==> dist(v 0,v 1) + t IN real_interval(a,b))` (C SUBGOAL_THEN MP_TAC);
    INTRO_TAC Zlzthic.real_interval_contains_0_ball [`a-dist(v 0,v 1)`;`b - dist(v 0,v 1)`;`&1`];
    REWRITE_TAC[arith `&0 < &1`;arith `a - d < &0 <=> a < d`;arith `&0 < b - d <=> d < b`];
    ANTS_TAC;
      FIRST_X_ASSUM_ST `dist s IN real_interval (a,b)` MP_TAC;
      BY(REWRITE_TAC[IN_REAL_INTERVAL]);
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `e'''` EXISTS_TAC;
    (ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC THEN (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_REAL_INTERVAL]);
    BY(REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `?t. (t < &0) /\ abs t < e2 /\  taum (norm (v 3)) (norm (v 0)) (norm (v 1)) (dist(v 0, v 1)) (dist (v 1,v 3))      (dist (v 0,v 3)) <=     taum (norm (v 3)) (norm (v 0)) (norm (v 1)) (dist (v 0,v 1) + t) (dist (v 1,v 3))     (dist (v 0,v 3))` ENOUGH_TO_SHOW_TAC;
    REPEAT WEAKER_STRIP_TAC;
    GEXISTL_TAC [`dist(v 0,v 1) + t`;`dist(v 0,v 1)`];
    ASM_REWRITE_TAC[];
    CONJ2_TAC;
      BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  COMMENT "choose epsilon and t";
  INTRO_TAC epsilon_hex [`e`;`e'`;`e''`;`e1`;`e1'`;`e2`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  TYPIFY `?t. t < &0 /\ abs t < e6` (C SUBGOAL_THEN MP_TAC);
    TYPIFY `-- e6 / &2` EXISTS_TAC;
    BY(FIRST_X_ASSUM_ST `&0 < e6` MP_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  REPLICATE_TAC 6 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  TYPIFY `t` EXISTS_TAC THEN ASM_REWRITE_TAC[];
  REPLICATE_TAC 8 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `rho_fun` MP_TAC THEN ASM_REWRITE_TAC[Appendix.rho_rho_fun];
  REWRITE_TAC[arith `r0 * (a013 + a034) + r1 * (a123 + a130) + r2 * a231 + r3 * (a340 + a301+a312) + r4 * a403 <=           r0 * (f013 + a034) + r1 * (a123 + f130) + r2 * a231 + r3 *(a340+f301 +a312) + r4*a403 <=>           r0 * a013 + r1*a130 + r3* a301 <=          r0 * f013 + r1 * f130 + r3 * f301`];
  MATCH_MP_TAC (arith `a - (pi+sol0) = a' /\ b - (pi+sol0) = b' ==> (a <= b ==> a' <= b')`);
  REWRITE_TAC[arith `(a + b+c) - (pi + sol0) = a + b + c - (pi + sol0)`];
  CONJ_TAC;
    GMATCH_SIMP_TAC (GSYM Cuxvzoz.tau3_azim);
    GMATCH_SIMP_TAC Cuxvzoz.tau3_taum_nonplanar;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[DIST_SYM];
    CONJ2_TAC;
      BY(MESON_TAC[Terminal.taum_sym]);
    BY(REPEAT (FIRST_X_ASSUM_ST `a < pi` MP_TAC) THEN REAL_ARITH_TAC);
  FIRST_X_ASSUM_ST `norm a  = norm b` (SUBST1_TAC o GSYM);
  TYPIFY `dist(v 0,v 1) + t = dist(v 0,v 1) + -- abs t` (C SUBGOAL_THEN SUBST1_TAC);
    BY(FIRST_X_ASSUM_ST `t < &0` MP_TAC THEN REAL_ARITH_TAC);
  FIRST_X_ASSUM_ST `d = d' + -- abs t` (SUBST1_TAC o GSYM);
  GMATCH_SIMP_TAC (GSYM Cuxvzoz.tau3_azim);
  GMATCH_SIMP_TAC Cuxvzoz.tau3_taum_nonplanar;
  REWRITE_TAC[DIST_SYM];
  REWRITE_TAC[CONJ_ASSOC] THEN CONJ2_TAC;
    ASM_REWRITE_TAC[DIST_SYM];
    BY(MESON_TAC[Terminal.taum_sym]);
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM_ST `a < pi` MP_TAC;
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

end;;