text_formalization/local/IUNBUIG.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Section: Appendix, Main Estimate, check_completeness                       *)
   4 (* Chapter: Local Fan                                                         *)
   5 (* Lemma: IUNBUIG                                                             *)
   6 (* Author: Thomas Hales                                                       *)
   7 (* Date: 2013-07-29                                                           *)
   8 (* ========================================================================== *)
   9
  10 module Iunbuig = struct
  11
  12
  13 open Hales_tactic;;
  14
  15
  16 let LET_THM = CONJ LET_DEF LET_END_DEF;;
  17
  18
  19 let quadratic_at_most_2_roots = prove_by_refinement(
  20   `!a b c. ?x1 x2. !x.
  21     ~(a = &0) /\ a * x pow 2 + b * x + c = &0 ==> x = x1 \/ x = x2`,
  22   (* {{{ proof *)
  23   [
  24   REPEAT GEN_TAC;
  25   ASM_CASES_TAC `~(?x1. a * x1 pow 2 + b * x1 + c = &0)`;
  26     BY(ASM_MESON_TAC[]);
  27   FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC;
  28   ASM_CASES_TAC `!x2. a * x2 pow 2 + b * x2 + c = &0 ==> x2 = x1`;
  29     BY(ASM_MESON_TAC[]);
  30   FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM] THEN REPEAT STRIP_TAC;
  31   GEXISTL_TAC [`x1`;`x2`];
  32   BY(GEN_TAC THEN ASM_TAC THEN CONV_TAC REAL_RING)
  33 (* String.length above = 414. String.length below = 233. 56% the length. *)
  34 (*
  35 g/r
  36 asmcs `~(?x1. a * x1 pow 2 + b * x1 + c = &0)`
  37 amt[]
  38 fx mp then rt[] then str/r
  39 asmcs `!x2. a * x2 pow 2 + b * x2 + c = &0 ==> x2 = x1`
  40 amt[]
  41 fx mp then rt[NOT_FORALL_THM] then str/r
  42 exl [`x1`;`x2`]
  43 g then asm then cvc REAL_RING
  44 *)
  45 (*
  46 If there are no roots, it is obvious. Otherwise, let x1 be a root.
  47 If every root is x1 it is obvious. Otherwise, let x2 be a second root.
  48 Instantiate the existential quantifiers with these two roots, and solve the resulting
  49 problem by Groebner basis algorithm.
  50 *)
  51 ]);;
  52   (* }}} *)
  53
  54 let ARCV_ADD_AFF_GE = prove_by_refinement(
  55   `!(u:real^N) v w x. ~(v = u) /\ ~(w = u) /\ ~(x = u) /\ x IN aff_ge {u} {v, w} ==>
  56     arcV u v x + arcV u x w = arcV u v w`,
  57   (* {{{ proof *)
  58   [
  59     BY(REWRITE_TAC[ARCV_ANGLE;ANGLES_ADD_AFF_GE])
  60   ]);;
  61   (* }}} *)
  62
  63 let SUM_NUMSEG4 = prove_by_refinement(
  64   `!t. sum (0..4) t = t 0 + t 1 + t 2 + t 3 + t 4`,
  65   (* {{{ proof *)
  66   [
  67   REWRITE_TAC[arith `4 = SUC 3`;SUM_CLAUSES_NUMSEG;Qknvmlb.SUM_NUMSEG3;arith `0 <= SUC 3`];
  68   BY(REAL_ARITH_TAC)
  69   ]);;
  70   (* }}} *)
  71
  72 let epsilon_pent = prove_by_refinement(
  73   `!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''''))`,
  74   (* {{{ proof *)
  75   [
  76   REPEAT WEAKER_STRIP_TAC;
  77   INTRO_TAC Cuxvzoz.epsilon_quad [`e`;`e'`;`e''`;`e'''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  78   INTRO_TAC Cuxvzoz.epsilon_pair [`e''''`;`e'''''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  79   TYPIFY `e''''''` EXISTS_TAC;
  80   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[])
  81   ]);;
  82   (* }}} *)
  83
  84 let epsilon_hex = prove_by_refinement(
  85   `!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))`,
  86   (* {{{ proof *)
  87   [
  88   REPEAT WEAKER_STRIP_TAC;
  89   INTRO_TAC epsilon_pent [`e`;`e'`;`e''`;`e'''`;`e''''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  90   INTRO_TAC Cuxvzoz.epsilon_pair [`e'''''`;`e5`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  91   TYPIFY `e''''''` EXISTS_TAC;
  92   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[])
  93   ]);;
  94   (* }}} *)
  95
  96 let epsilon_hept = prove_by_refinement(
  97   `!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))`,
  98   (* {{{ proof *)
  99   [
 100   REPEAT WEAKER_STRIP_TAC;
 101   INTRO_TAC epsilon_hex [`e`;`e'`;`e''`;`e'''`;`e''''`;`e5`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
 102   INTRO_TAC Cuxvzoz.epsilon_pair [`e6`;`e6'`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
 103   TYPIFY `e'''''` EXISTS_TAC;
 104   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[])
 105   ]);;
 106   (* }}} *)
 107
 108 let re_eqvl_imp_le = prove_by_refinement(
 109   `!a b. re_eqvl a b ==> (&0 <= a <=> &0 <= b)`,
 110   (* {{{ proof *)
 111   [
 112   TYPIFY `!a b. re_eqvl a b /\ &0 <= b ==> &0 <= a` ENOUGH_TO_SHOW_TAC;
 113     BY(MESON_TAC[Leaf_cell.RE_EQVL_SYM]);
 114   REWRITE_TAC[Trigonometry2.re_eqvl];
 115   REPEAT WEAKER_STRIP_TAC;
 116   ASM_REWRITE_TAC[];
 117   GMATCH_SIMP_TAC REAL_LE_MUL;
 118   BY(ASM_TAC THEN REAL_ARITH_TAC)
 119   ]);;
 120   (* }}} *)
 121
 122 let re_eqvl_real_sgn = prove_by_refinement(
 123   `!x y. re_eqvl x y <=> real_sgn x = real_sgn y`,
 124   (* {{{ proof *)
 125   [
 126   REPEAT WEAKER_STRIP_TAC;
 127   MATCH_MP_TAC (TAUT `((a ==>b) /\ (b ==> a)) ==> (a = b)`);
 128   REWRITE_TAC[Trigonometry2.re_eqvl];
 129   CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[];
 130     REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[REAL_SGN_MUL;GSYM REAL_SGN_EQ;arith `&0 < t <=> t > &0`];
 131     BY(DISCH_THEN (unlist REWRITE_TAC) THEN REAL_ARITH_TAC);
 132   FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[REAL_SGN];
 133   TYPIFY `x = &0` ASM_CASES_TAC;
 134     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`];
 135     BY(MESON_TAC[arith `&0 < &1`]);
 136   DISCH_TAC;
 137   TYPIFY `~(y = &0)` (C SUBGOAL_THEN ASSUME_TAC);
 138     DISCH_TAC;
 139     FIRST_X_ASSUM_ST `abs` MP_TAC;
 140     BY(ASM_REWRITE_TAC[arith `&0 / t = &0`;REAL_DIV_EQ_0] THEN ASM_TAC THEN REAL_ARITH_TAC);
 141   TYPIFY `x / y` EXISTS_TAC;
 142   CONJ2_TAC;
 143     Calc_derivative.CALC_ID_TAC;
 144     BY(ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
 145   REWRITE_TAC[Calc_derivative.invert_den_lt];
 146   REWRITE_TAC[REAL_MUL_POS_LT];
 147   FIRST_X_ASSUM_ST `abs` MP_TAC THEN REWRITE_TAC[GSYM REAL_SGN;real_sgn];
 148   RULE_ASSUM_TAC (REWRITE_RULE[arith `~(x = &0) <=> (&0 < x \/ x < &0) /\ ~(&0 < x /\ x < &0)`]);
 149   ASSUME_TAC (arith ` ~(&1 = -- &1)`);
 150   BY(REPEAT COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[])
 151   ]);;
 152   (* }}} *)
 153
 154 let coplanar_delta_y_zero = prove_by_refinement(
 155   `!(u0:real^3) u1 u2 u3. coplanar  {u0, u1, u2, u3} <=>
 156             delta_y (dist (u0,u1)) (dist (u0,u2)) (dist (u0,u3))
 157             (dist (u2,u3))
 158             (dist (u1,u3))
 159             (dist (u1,u2)) = &0`,
 160   (* {{{ proof *)
 161   [
 162   REPEAT WEAKER_STRIP_TAC;
 163   BY(ASM_MESON_TAC[Terminal.DELTA_Y_POS_4POINTS;Oxlzlez.coplanar_delta_y;arith `&0 <= x ==> (~(&0 < x) <=> (x = &0))`])
 164   ]);;
 165   (* }}} *)
 166
 167 let real_continuous_finite_range_constant = prove_by_refinement(
 168   `!f a b. f real_continuous_on (real_interval (a,b)) /\ FINITE (IMAGE f (real_interval (a,b))) ==>
 169     (?c. !x. x IN real_interval (a,b) ==> f x = c)`,
 170   (* {{{ proof *)
 171   [
 172   REPEAT WEAKER_STRIP_TAC;
 173   TYPIFY `(?c. !x. x IN IMAGE lift (real_interval(a,b)) ==> ((lift o f o drop) x = c))` ENOUGH_TO_SHOW_TAC;
 174     REPEAT WEAKER_STRIP_TAC;
 175     TYPIFY `drop c` EXISTS_TAC;
 176     REPEAT WEAKER_STRIP_TAC;
 177     FIRST_X_ASSUM_ST `IMAGE` (C INTRO_TAC [`lift x`]);
 178     REWRITE_TAC[o_THM;LIFT_DROP];
 179     ANTS_TAC;
 180       MATCH_MP_TAC FUN_IN_IMAGE;
 181       BY(ASM_REWRITE_TAC[]);
 182     DISCH_THEN (SUBST1_TAC o GSYM);
 183     BY(REWRITE_TAC[LIFT_DROP]);
 184   MATCH_MP_TAC CONTINUOUS_FINITE_RANGE_CONSTANT;
 185   CONJ_TAC;
 186     ONCE_REWRITE_TAC[GSYM LIFT_DROP];
 187     REWRITE_TAC[GSYM INTERVAL_REAL_INTERVAL];
 188     BY(REWRITE_TAC[CONNECTED_INTERVAL]);
 189   CONJ_TAC;
 190     REWRITE_TAC[ETA_AX];
 191     BY(ASM_REWRITE_TAC[GSYM REAL_CONTINUOUS_ON]);
 192   REWRITE_TAC[GSYM IMAGE_o;ETA_AX;GSYM o_ASSOC];
 193   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);
 194     BY(REWRITE_TAC[GSYM IMAGE_o;GSYM o_ASSOC]);
 195   REWRITE_TAC[IMAGE_LIFT_DROP];
 196   MATCH_MP_TAC FINITE_IMAGE;
 197   BY(ASM_REWRITE_TAC[])
 198   ]);;
 199   (* }}} *)
 200
 201 let planar_deform_dist = prove_by_refinement(
 202   `!(v0:real^3) v1 v2 f V e'.
 203     v1 IN V /\ v2 IN V /\ ~(v0 = vec 0) /\
 204     &0 < e' /\ deformation f V (--e',e') /\ (!v t. ~(v  =v1) /\ ~(v = v2) ==> f v t = v) /\
 205 (!t. abs t < e'
 206                  ==> coplanar {vec 0, v0, f v1 t, f v2 t} /\
 207                      dist (v0,f v1 t) = dist (v0,v1) /\
 208                      norm (f v1 t) = norm v1 /\
 209                      dist (f v2 t,v0) = dist (v2,v0) /\
 210                      norm (f v2 t) = norm v2) ==>
 211     (!t. abs t < e' ==> dist(f v1 t,f v2 t) = dist(v1,v2))
 212 `,
 213   (* {{{ proof *)
 214   [
 215   REPEAT WEAKER_STRIP_TAC;
 216   TYPIFY `f v1 (&0) = v1 /\ f v2 (&0) = v2` (C SUBGOAL_THEN ASSUME_TAC);
 217     FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
 218     BY(ASM_MESON_TAC[]);
 219   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)))`;
 220   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))`;
 221   TYPED_ABBREV_TAC `a = (norm v0 * norm v0)`;
 222   INTRO_TAC quadratic_at_most_2_roots [`a`;`b`;`c`];
 223   REPEAT WEAKER_STRIP_TAC;
 224   INTRO_TAC real_continuous_finite_range_constant [`(\t. dist(f v1 t, f v2 t))`;`-- e'`;`e'`];
 225   ANTS_TAC;
 226     CONJ_TAC;
 227       GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
 228       REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
 229       REPEAT WEAKER_STRIP_TAC;
 230       MATCH_MP_TAC Local_lemmas1.CON_ATREAL_REAL_CON2_REDO;
 231       FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation;ETA_AX];
 232       BY(ASM_MESON_TAC[]);
 233     TYPIFY `IMAGE (\t. dist (f v1 t,f v2 t) pow 2) (real_interval (--e',e')) SUBSET {x1,x2}` ENOUGH_TO_SHOW_TAC;
 234       TYPIFY `FINITE {x1,x2}` ENOUGH_TO_SHOW_TAC;
 235         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);
 236           REWRITE_TAC[GSYM IMAGE_o];
 237           BY(GEN_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM;o_THM]);
 238         TYPED_ABBREV_TAC `s = (IMAGE (\t. dist (f v1 t,f v2 t)) (real_interval (--e',e')))`;
 239         INTRO_TAC HAS_SIZE_IMAGE_INJ_EQ [`(\t. t pow 2)`;`s`;`CARD (IMAGE (\t. t pow 2) s)`];
 240         ANTS_TAC;
 241           EXPAND_TAC "s";
 242           REWRITE_TAC[IN_IMAGE] THEN REPEAT WEAKER_STRIP_TAC;
 243           FIRST_X_ASSUM MP_TAC;
 244           ASM_REWRITE_TAC[];
 245           REWRITE_TAC[GSYM REAL_EQ_SQUARE_ABS];
 246           REPEAT (GMATCH_SIMP_TAC (arith `&0 <= x ==> abs x = x`));
 247           BY(REWRITE_TAC[DIST_POS_LE]);
 248         REWRITE_TAC[HAS_SIZE];
 249         BY(MESON_TAC[FINITE_SUBSET;FINITE_IMAGE]);
 250       BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
 251     REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_IMAGE];
 252     REPEAT WEAKER_STRIP_TAC;
 253     FIRST_X_ASSUM MATCH_MP_TAC;
 254     CONJ_TAC;
 255       EXPAND_TAC "a";
 256       REWRITE_TAC[REAL_ENTIRE];
 257       REWRITE_TAC[NORM_EQ_0];
 258       BY(ASM_REWRITE_TAC[]);
 259     FIRST_X_ASSUM_ST `coplanar` (C INTRO_TAC [`x'`]);
 260     ANTS_TAC;
 261       BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[IN_REAL_INTERVAL;arith `-- e < t /\ t < e <=> abs t < e`]);
 262     REPEAT WEAKER_STRIP_TAC;
 263     FIRST_X_ASSUM_ST `coplanar` MP_TAC THEN REWRITE_TAC[coplanar_delta_y_zero];
 264     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[];
 265     ONCE_REWRITE_TAC[arith `x = &0 <=> -- x = &0`];
 266     ASM_REWRITE_TAC[Sphere.delta_y;Nonlinear_lemma.delta_quadratic];
 267     BY(REAL_ARITH_TAC);
 268   REPEAT WEAKER_STRIP_TAC;
 269   FIRST_ASSUM (C INTRO_TAC [`&0`]);
 270   FIRST_X_ASSUM (C INTRO_TAC [`t`]);
 271   REWRITE_TAC[];
 272   REPEAT (DISCH_THEN GMATCH_SIMP_TAC);
 273   ASM_REWRITE_TAC[];
 274   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`];
 275   BY(ASM_MESON_TAC[])
 276   ]);;
 277   (* }}} *)
 278
 279 (*
 280 let deform_pent_exists = prove_by_refinement(
 281   `!V g23 v0 v1 v2 v3 e. ?f.
 282     (
 283        (    v1 IN V /\ v2 IN V /\
 284               (coplanar {vec 0,v0,v1,v2} ==> (v1 cross v0) dot (v2 cross v0) > &0) /\
 285                         ~coplanar {vec 0,v0,v2,v3} /\ ~(collinear {vec 0,v1,v2}) /\
 286           &0 < azim (vec 0) v1 v2 v0 /\ azim (vec 0) v1 v2 v0 <= pi /\
 287           v2 dot (v3 cross v0) > &0 /\
 288           &0 < e /\
 289           g23 real_continuous_on (real_interval (--e,e)) /\
 290           g23 (&0) = &0
 291         ==>
 292           (?e'. &0 < e' /\ deformation f V (-- e', e') /\
 293              (!v t. ~(v = v1) /\ ~(v = v2) ==> f v t = v) /\
 294              (!t. abs t < e' ==>
 295                 dist(v0,f v1 t) = dist(v0,v1) /\
 296                 dist(f v2 t,f v1 t) = dist(v2,v1) /\
 297                 norm(f v1 t) = norm(v1) /\
 298                   dist (f v2 t,v0) = dist(v2,v0) /\
 299                   dist (f v2 t,v3) = dist(v2,v3)+ g23 t /\
 300                   norm(f v2 t) = norm (v2)
 301              ))))`,
 302   (* {{{ proof *)
 303   [
 304   REPEAT WEAKER_STRIP_TAC;
 305   REWRITE_TAC[MESON [] `(?f. a ==> P f) <=> (a ==> (?f. P f))`];
 306   REPEAT WEAKER_STRIP_TAC;
 307   TYPIFY `~coplanar {vec 0,v0,v1,v2}` ASM_CASES_TAC;
 308     INTRO_TAC Cuxvzoz.deform_684_pent_exists [`V`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
 309     REPEAT WEAKER_STRIP_TAC;
 310     FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[];
 311     REWRITE_TAC[arith `x > &0 <=> &0 <= x /\ ~(x = &0)`];
 312     ANTS_TAC;
 313       ASM_REWRITE_TAC[];
 314       CONJ2_TAC;
 315         BY(REPEAT (FIRST_X_ASSUM_ST `coplanar` MP_TAC) THEN REWRITE_TAC[GSYM Local_lemmas.CROSS_DOT_COPLANAR] THEN VEC3_TAC);
 316       INTRO_TAC Trigonometry2.JBDNJJB [`v1`;`v2`;`v0`];
 317       TYPIFY `((v1 cross v2) dot v0) = v1 dot (v2 cross v0)` (C SUBGOAL_THEN SUBST1_TAC);
 318         BY(VEC3_TAC);
 319       ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
 320       DISCH_THEN ((unlist REWRITE_TAC) o (MATCH_MP re_eqvl_imp_le));
 321       BY(ASM_MESON_TAC[Local_lemmas.SIN_AZIM_POS_PI_LT]);
 322     REPEAT WEAKER_STRIP_TAC;
 323     BY(GEXISTL_TAC [`f`;`e'`] THEN ASM_MESON_TAC[]);
 324   COMMENT "planar case";
 325   INTRO_TAC Cuxvzoz.deform_planar_exists [`V`;`(\ (t:real). &0)`;`(\ (t:real). &0)`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
 326   RULE_ASSUM_TAC(REWRITE_RULE[]);
 327   REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[arith `x + &0 = x`];
 328   GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;Ocbicby.REAL_OPEN_REAL_INTERVAL];
 329   ANTS_TAC;
 330     CONJ_TAC;
 331       BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
 332     BY(FIRST_X_ASSUM_ST `collinear` MP_TAC THEN MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b} = {a,b}`]);
 333   REPEAT WEAKER_STRIP_TAC;
 334   GEXISTL_TAC [`f`;`e'`] THEN ASM_REWRITE_TAC[];
 335   REPEAT WEAKER_STRIP_TAC;
 336   TYPIFY `~(v0 = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
 337     BY(ASM_MESON_TAC[COPLANAR_3;SET_RULE `{a,a,b,c} = {a,b,c}`]);
 338   INTRO_TAC planar_deform_dist [`v0`;`v1`;`v2`;`f`;`V`;`e'`];
 339   ASM_REWRITE_TAC[];
 340   ANTS_TAC;
 341     BY(ASM_MESON_TAC[]);
 342   DISCH_TAC;
 343   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[])
 344   ]);;
 345   (* }}} *)
 346 *)
 347
 348 (*
 349 let deform_pent_exists = prove_by_refinement(
 350   `!V g23 v0 v1 v2 v3 e. ?f.
 351     (
 352        (    v1 IN V /\ v2 IN V /\
 353               (coplanar {vec 0,v0,v1,v2} ==> (v1 cross v0) dot (v2 cross v0) > &0) /\
 354                         ~coplanar {vec 0,v0,v2,v3} /\ ~(collinear {vec 0,v1,v2}) /\
 355               azim (vec 0) v1 v2 v0 <= pi /\
 356           v2 dot (v3 cross v0) > &0 /\
 357           &0 < e /\
 358           g23 real_continuous_on (real_interval (--e,e)) /\
 359           g23 (&0) = &0
 360         ==>
 361           (?e'. &0 < e' /\ deformation f V (-- e', e') /\
 362              (!v t. ~(v = v1) /\ ~(v = v2) ==> f v t = v) /\
 363              (!t. abs t < e' ==>
 364                 dist(v0,f v1 t) = dist(v0,v1) /\
 365                 dist(f v2 t,f v1 t) = dist(v2,v1) /\
 366                 norm(f v1 t) = norm(v1) /\
 367                   dist (f v2 t,v0) = dist(v2,v0) /\
 368                   dist (f v2 t,v3) = dist(v2,v3)+ g23 t /\
 369                   norm(f v2 t) = norm (v2)
 370              ))))`,
 371   (* {{{ proof *)
 372   [
 373   REPEAT WEAKER_STRIP_TAC;
 374   REWRITE_TAC[MESON [] `(?f. a ==> P f) <=> (a ==> (?f. P f))`];
 375   REPEAT WEAKER_STRIP_TAC;
 376   TYPIFY `~coplanar {vec 0,v0,v1,v2}` ASM_CASES_TAC;
 377     INTRO_TAC Cuxvzoz.deform_684_pent_exists [`V`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
 378     REPEAT WEAKER_STRIP_TAC;
 379     FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[];
 380     REWRITE_TAC[arith `x > &0 <=> &0 <= x /\ ~(x = &0)`];
 381     ANTS_TAC;
 382       ASM_REWRITE_TAC[];
 383       CONJ2_TAC;
 384         BY(REPEAT (FIRST_X_ASSUM_ST `coplanar` MP_TAC) THEN REWRITE_TAC[GSYM Local_lemmas.CROSS_DOT_COPLANAR] THEN VEC3_TAC);
 385       INTRO_TAC Trigonometry2.JBDNJJB [`v1`;`v2`;`v0`];
 386       TYPIFY `((v1 cross v2) dot v0) = v1 dot (v2 cross v0)` (C SUBGOAL_THEN SUBST1_TAC);
 387         BY(VEC3_TAC);
 388       ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
 389       DISCH_THEN ((unlist REWRITE_TAC) o (MATCH_MP re_eqvl_imp_le));
 390       BY(ASM_MESON_TAC[Local_lemmas.SIN_AZIM_POS_PI_LT]);
 391     REPEAT WEAKER_STRIP_TAC;
 392     BY(GEXISTL_TAC [`f`;`e'`] THEN ASM_MESON_TAC[]);
 393   COMMENT "planar case";
 394   INTRO_TAC Cuxvzoz.deform_planar_exists [`V`;`(\ (t:real). &0)`;`(\ (t:real). &0)`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
 395   RULE_ASSUM_TAC(REWRITE_RULE[]);
 396   REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[arith `x + &0 = x`];
 397   GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;Ocbicby.REAL_OPEN_REAL_INTERVAL];
 398   ANTS_TAC;
 399     CONJ_TAC;
 400       BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
 401     BY(FIRST_X_ASSUM_ST `collinear` MP_TAC THEN MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b} = {a,b}`]);
 402   REPEAT WEAKER_STRIP_TAC;
 403   GEXISTL_TAC [`f`;`e'`] THEN ASM_REWRITE_TAC[];
 404   REPEAT WEAKER_STRIP_TAC;
 405   TYPIFY `~(v0 = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
 406     BY(ASM_MESON_TAC[COPLANAR_3;SET_RULE `{a,a,b,c} = {a,b,c}`]);
 407   INTRO_TAC planar_deform_dist [`v0`;`v1`;`v2`;`f`;`V`;`e'`];
 408   ASM_REWRITE_TAC[];
 409   ANTS_TAC;
 410     BY(ASM_MESON_TAC[]);
 411   DISCH_TAC;
 412   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[])
 413   ]);;
 414   (* }}} *)
 415 *)
 416
 417 let deform_pent_exists = prove_by_refinement(
 418   `!V g23 v0 v1 v2 v3 e. ?f.
 419            v1 IN V /\ v2 IN V /\
 420               (coplanar {vec 0,v0,v1,v2} ==> (v1 cross v0) dot (v2 cross v0) > &0) /\
 421                         ~coplanar {vec 0,v0,v2,v3} /\ ~(collinear {vec 0,v1,v2}) /\
 422               azim (vec 0) v1 v2 v0 <= pi /\
 423           v2 dot (v3 cross v0) > &0 /\
 424           &0 < e /\
 425           g23 real_continuous_on (real_interval (--e,e)) /\
 426           g23 (&0) = &0
 427         ==>
 428           (?e'. &0 < e' /\ deformation f V (-- e', e') /\
 429              (!v t. ~(v = v1) /\ ~(v = v2) ==> f v t = v) /\
 430              (!t. abs t < e' ==>
 431                 dist(v0,f v1 t) = dist(v0,v1) /\
 432                 dist(f v2 t,f v1 t) = dist(v2,v1) /\
 433                 norm(f v1 t) = norm(v1) /\
 434                   dist (f v2 t,v0) = dist(v2,v0) /\
 435                   dist (f v2 t,v3) = dist(v2,v3)+ g23 t /\
 436                   norm(f v2 t) = norm (v2) /\
 437                   (coplanar {vec 0,v0,v1,v2} ==> coplanar {vec 0,v0,f v1 t,f v2 t})
 438              ))`,
 439   (* {{{ proof *)
 440   [
 441   REPEAT WEAKER_STRIP_TAC;
 442   REWRITE_TAC[MESON [] `(?f. a ==> P f) <=> (a ==> (?f. P f))`];
 443   REPEAT WEAKER_STRIP_TAC;
 444   TYPIFY `~coplanar {vec 0,v0,v1,v2}` ASM_CASES_TAC;
 445     INTRO_TAC Cuxvzoz.deform_684_pent_exists [`V`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
 446     REPEAT WEAKER_STRIP_TAC;
 447     FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[];
 448     REWRITE_TAC[arith `x > &0 <=> &0 <= x /\ ~(x = &0)`];
 449     ANTS_TAC;
 450       ASM_REWRITE_TAC[];
 451       CONJ2_TAC;
 452         BY(REPEAT (FIRST_X_ASSUM_ST `coplanar` MP_TAC) THEN REWRITE_TAC[GSYM Local_lemmas.CROSS_DOT_COPLANAR] THEN VEC3_TAC);
 453       INTRO_TAC Trigonometry2.JBDNJJB [`v1`;`v2`;`v0`];
 454       TYPIFY `((v1 cross v2) dot v0) = v1 dot (v2 cross v0)` (C SUBGOAL_THEN SUBST1_TAC);
 455         BY(VEC3_TAC);
 456       ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
 457       DISCH_THEN ((unlist REWRITE_TAC) o (MATCH_MP re_eqvl_imp_le));
 458       BY(ASM_MESON_TAC[Local_lemmas.SIN_AZIM_POS_PI_LT]);
 459     REPEAT WEAKER_STRIP_TAC;
 460     BY(GEXISTL_TAC [`f`;`e'`] THEN ASM_MESON_TAC[]);
 461   COMMENT "planar case";
 462   INTRO_TAC Cuxvzoz.deform_planar_exists [`V`;`(\ (t:real). &0)`;`(\ (t:real). &0)`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
 463   RULE_ASSUM_TAC(REWRITE_RULE[]);
 464   REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[arith `x + &0 = x`];
 465   GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;Ocbicby.REAL_OPEN_REAL_INTERVAL];
 466   ANTS_TAC;
 467     CONJ_TAC;
 468       BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
 469     BY(FIRST_X_ASSUM_ST `collinear` MP_TAC THEN MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b} = {a,b}`]);
 470   REPEAT WEAKER_STRIP_TAC;
 471   GEXISTL_TAC [`f`;`e'`] THEN ASM_REWRITE_TAC[];
 472   REPEAT WEAKER_STRIP_TAC;
 473   TYPIFY `~(v0 = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
 474     BY(ASM_MESON_TAC[COPLANAR_3;SET_RULE `{a,a,b,c} = {a,b,c}`]);
 475   INTRO_TAC planar_deform_dist [`v0`;`v1`;`v2`;`f`;`V`;`e'`];
 476   ASM_REWRITE_TAC[];
 477   ANTS_TAC;
 478     BY(ASM_MESON_TAC[]);
 479   DISCH_TAC;
 480   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[])
 481   ]);;
 482   (* }}} *)
 483
 484 (*
 485 let EGHNAVX_SCS = prove_by_refinement(
 486   `!s k v p.
 487     (let bta = (\j.  azim (vec 0) (v p) (v (p+1)) (v (p+j))) in
 488     (    is_scs_v39 s /\ scs_k_v39 s = k /\
 489         3 < k /\
 490          BBs_v39 s v /\
 491         scs_basic_v39 s /\
 492          scs_generic v ==>
 493            bta 1 = &0 /\
 494             bta (k - 1) <= pi /\
 495             (!i j. i < j /\ j < k ==> bta i <= bta j) /\
 496             (!q j. bta q = &0 /\ 0 < j /\ j <= q /\ q < k
 497                       ==> (j<q ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v (p+j+k-1)) = pi) /\
 498                   v (p+j) IN aff_gt {vec 0,v p} {v (p+1)}) /\
 499             (!q j. bta q = bta (k - 1) /\ 0 < q /\ q < k - 1 /\ q <= j /\ j < k
 500                       ==> (q < j ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v(p+j+k-1)) = pi) /\
 501                   v(p+j) IN aff_gt {vec 0, v p} {v (p + k - 1)})))`,
 502   (* {{{ proof *)
 503   [
 504   REPEAT GEN_TAC;
 505   LET_TAC;
 506   REPEAT WEAKER_STRIP_TAC;
 507   TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
 508   TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
 509   TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
 510   INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`k`];
 511   ASM_REWRITE_TAC[];
 512   DISCH_TAC;
 513   TYPIFY `periodic v k /\ convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 514     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)`]);
 515   INTRO_TAC Terminal.ITER_vv_rho_node1 [`v`;`k`];
 516   ASM_REWRITE_TAC[LET_THM];
 517   TYPIFY_GOAL_THEN `3 <= k` (unlist REWRITE_TAC);
 518     BY(ASM_MESON_TAC[arith `3 < k ==> 3 <= k`]);
 519   DISCH_TAC;
 520   INTRO_TAC (GEN_ALL Odxlstcv2.CARD_V_EQ_SCS_K1) [`s`;`v`;`V`;`k`];
 521   ASM_REWRITE_TAC[];
 522   DISCH_TAC;
 523   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 524     MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
 525     BY(ASM_REWRITE_TAC[]);
 526   TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
 527     GEN_TAC;
 528     EXPAND_TAC "V";
 529     MATCH_MP_TAC FUN_IN_IMAGE;
 530     BY(REWRITE_TAC[IN_UNIV]);
 531   TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0, v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
 532     INTRO_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN [`V`;`E`;`FF`];
 533     BY(ASM_MESON_TAC[Appendix.scs_generic]);
 534   INTRO_TAC (GENL [`v0:real^3`;`vv:num->real^3`;`i:num`] Local_lemmas.EGHNAVX) [`v p`;`\ (i:num). v (p + i)`];
 535   REWRITE_TAC[RIGHT_FORALL_IMP_THM;GSYM RIGHT_AND_FORALL_THM];
 536   ASM_REWRITE_TAC[];
 537   ANTS_TAC;
 538     CONJ_TAC;
 539       REPEAT WEAKER_STRIP_TAC;
 540       TYPIFY `?i'. v' = v i'` (C SUBGOAL_THEN MP_TAC);
 541         FIRST_X_ASSUM_ST `IN` MP_TAC;
 542         EXPAND_TAC "V";
 543         BY(REWRITE_TAC[IN_IMAGE;IN_UNIV]);
 544       REPEAT WEAKER_STRIP_TAC;
 545       BY(ASM_MESON_TAC[]);
 546     EXPAND_TAC "bta";
 547     BY(REWRITE_TAC[]);
 548   REPEAT WEAKER_STRIP_TAC;
 549   ASM_REWRITE_TAC[];
 550   INTRO_TAC (GSYM Ocbicby.INTERIOR_ANGLE1_AZIM) [`s`;`v`];
 551   ASM_REWRITE_TAC[LET_THM];
 552   TYPIFY_GOAL_THEN `v IN BBs_v39 s` (unlist REWRITE_TAC);
 553     BY(ASM_REWRITE_TAC[IN]);
 554   DISCH_TAC;
 555   COMMENT "first conjunct";
 556   CONJ_TAC;
 557     REPEAT WEAKER_STRIP_TAC;
 558     FIRST_X_ASSUM_ST `SUBSET` (C INTRO_TAC [`q`]);
 559     ASM_REWRITE_TAC[];
 560     REPEAT WEAKER_STRIP_TAC;
 561     CONJ_TAC;
 562       DISCH_TAC;
 563       FIRST_X_ASSUM (C INTRO_TAC [`j`]);
 564       ASM_REWRITE_TAC[];
 565       BY(REWRITE_TAC[arith `SUC (p+j) = p+j+1 /\ ((p+j) + k - 1 = p+j+k-1)`]);
 566     FIRST_X_ASSUM kill;
 567     FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM];
 568     DISCH_THEN (C INTRO_TAC [`v (p+(j:num))`]);
 569     DISCH_THEN MATCH_MP_TAC;
 570     BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
 571   REPEAT WEAKER_STRIP_TAC;
 572   FIRST_X_ASSUM_ST `SUBSET` (C INTRO_TAC [`q`]);
 573   ASM_REWRITE_TAC[];
 574   REPEAT WEAKER_STRIP_TAC;
 575   CONJ_TAC;
 576     DISCH_TAC;
 577     FIRST_X_ASSUM (C INTRO_TAC [`j`]);
 578     ASM_REWRITE_TAC[];
 579     BY(REWRITE_TAC[arith `SUC (p+j) = p+j+1 /\ ((p+j) + k - 1 = p+j+k-1)`]);
 580   FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM];
 581   DISCH_THEN (C INTRO_TAC [`v (p+(j:num))`]);
 582   DISCH_THEN MATCH_MP_TAC;
 583   BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[])
 584   ]);;
 585   (* }}} *)
 586 *)
 587
 588 let EGHNAVX_COLL_SCS = prove_by_refinement(
 589   `!s k v p.
 590     (let bta = (\j.  azim (vec 0) (v p) (v (p+1)) (v (p+j))) in
 591     (    is_scs_v39 s /\ scs_k_v39 s = k /\
 592         3 < k /\
 593          BBs_v39 s v /\
 594         scs_basic_v39 s /\
 595         (!i. ~(v i = v p) ==> ~collinear {vec 0,v p,v i})
 596         ==>
 597            bta 1 = &0 /\
 598             bta (k - 1) <= pi /\
 599             (!i j. i < j /\ j < k ==> bta i <= bta j) /\
 600             (!q j. bta q = &0 /\ 0 < j /\ j <= q /\ q < k
 601                       ==> (j<q ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v (p+j+k-1)) = pi) /\
 602                   v (p+j) IN aff_gt {vec 0,v p} {v (p+1)}) /\
 603             (!q j. bta q = bta (k - 1) /\ 0 < q /\ q < k - 1 /\ q <= j /\ j < k
 604                       ==> (q < j ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v(p+j+k-1)) = pi) /\
 605                   v(p+j) IN aff_gt {vec 0, v p} {v (p + k - 1)})))`,
 606   (* {{{ proof *)
 607   [
 608   REPEAT GEN_TAC;
 609   LET_TAC;
 610   REPEAT WEAKER_STRIP_TAC;
 611   TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
 612   TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
 613   TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
 614   INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`k`];
 615   ASM_REWRITE_TAC[];
 616   DISCH_TAC;
 617   TYPIFY `periodic v k /\ convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 618     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)`]);
 619   INTRO_TAC Terminal.ITER_vv_rho_node1 [`v`;`k`];
 620   ASM_REWRITE_TAC[LET_THM];
 621   TYPIFY_GOAL_THEN `3 <= k` (unlist REWRITE_TAC);
 622     BY(ASM_MESON_TAC[arith `3 < k ==> 3 <= k`]);
 623   DISCH_TAC;
 624   INTRO_TAC (GEN_ALL Odxlstcv2.CARD_V_EQ_SCS_K1) [`s`;`v`;`V`;`k`];
 625   ASM_REWRITE_TAC[];
 626   DISCH_TAC;
 627   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 628     MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
 629     BY(ASM_REWRITE_TAC[]);
 630   TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
 631     GEN_TAC;
 632     EXPAND_TAC "V";
 633     MATCH_MP_TAC FUN_IN_IMAGE;
 634     BY(REWRITE_TAC[IN_UNIV]);
 635   INTRO_TAC (GENL [`v0:real^3`;`vv:num->real^3`;`i:num`] Local_lemmas.EGHNAVX) [`v p`;`\ (i:num). v (p + i)`];
 636   REWRITE_TAC[RIGHT_FORALL_IMP_THM;GSYM RIGHT_AND_FORALL_THM];
 637   ASM_REWRITE_TAC[];
 638   ANTS_TAC;
 639     CONJ_TAC;
 640       EXPAND_TAC "V";
 641       (REWRITE_TAC[IN_IMAGE;IN_UNIV]);
 642       BY(ASM_MESON_TAC[]);
 643     EXPAND_TAC "bta";
 644     BY(REWRITE_TAC[]);
 645   REPEAT WEAKER_STRIP_TAC;
 646   ASM_REWRITE_TAC[];
 647   INTRO_TAC (GSYM Ocbicby.INTERIOR_ANGLE1_AZIM) [`s`;`v`];
 648   ASM_REWRITE_TAC[LET_THM];
 649   TYPIFY_GOAL_THEN `v IN BBs_v39 s` (unlist REWRITE_TAC);
 650     BY(ASM_REWRITE_TAC[IN]);
 651   DISCH_TAC;
 652   COMMENT "first conjunct";
 653   CONJ_TAC;
 654     REPEAT WEAKER_STRIP_TAC;
 655     FIRST_X_ASSUM_ST `SUBSET` (C INTRO_TAC [`q`]);
 656     ASM_REWRITE_TAC[];
 657     REPEAT WEAKER_STRIP_TAC;
 658     CONJ_TAC;
 659       DISCH_TAC;
 660       FIRST_X_ASSUM (C INTRO_TAC [`j`]);
 661       ASM_REWRITE_TAC[];
 662       BY(REWRITE_TAC[arith `SUC (p+j) = p+j+1 /\ ((p+j) + k - 1 = p+j+k-1)`]);
 663     FIRST_X_ASSUM kill;
 664     FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM];
 665     DISCH_THEN (C INTRO_TAC [`v (p+(j:num))`]);
 666     DISCH_THEN MATCH_MP_TAC;
 667     BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
 668   REPEAT WEAKER_STRIP_TAC;
 669   FIRST_X_ASSUM_ST `SUBSET` (C INTRO_TAC [`q`]);
 670   ASM_REWRITE_TAC[];
 671   REPEAT WEAKER_STRIP_TAC;
 672   CONJ_TAC;
 673     DISCH_TAC;
 674     FIRST_X_ASSUM (C INTRO_TAC [`j`]);
 675     ASM_REWRITE_TAC[];
 676     BY(REWRITE_TAC[arith `SUC (p+j) = p+j+1 /\ ((p+j) + k - 1 = p+j+k-1)`]);
 677   FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM];
 678   DISCH_THEN (C INTRO_TAC [`v (p+(j:num))`]);
 679   DISCH_THEN MATCH_MP_TAC;
 680   BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[])
 681   ]);;
 682   (* }}} *)
 683
 684 let EGHNAVX_SCS = prove_by_refinement(
 685   `!s k v p.
 686     (let bta = (\j.  azim (vec 0) (v p) (v (p+1)) (v (p+j))) in
 687     (    is_scs_v39 s /\ scs_k_v39 s = k /\
 688         3 < k /\
 689          BBs_v39 s v /\
 690         scs_basic_v39 s /\
 691          scs_generic v ==>
 692            bta 1 = &0 /\
 693             bta (k - 1) <= pi /\
 694             (!i j. i < j /\ j < k ==> bta i <= bta j) /\
 695             (!q j. bta q = &0 /\ 0 < j /\ j <= q /\ q < k
 696                       ==> (j<q ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v (p+j+k-1)) = pi) /\
 697                   v (p+j) IN aff_gt {vec 0,v p} {v (p+1)}) /\
 698             (!q j. bta q = bta (k - 1) /\ 0 < q /\ q < k - 1 /\ q <= j /\ j < k
 699                       ==> (q < j ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v(p+j+k-1)) = pi) /\
 700                   v(p+j) IN aff_gt {vec 0, v p} {v (p + k - 1)})))`,
 701   (* {{{ proof *)
 702   [
 703   REWRITE_TAC[LET_THM];
 704   REPEAT WEAKER_STRIP_TAC;
 705   MATCH_MP_TAC (REWRITE_RULE[LET_THM] EGHNAVX_COLL_SCS);
 706   TYPIFY `s` EXISTS_TAC;
 707   ASM_REWRITE_TAC[];
 708   REPEAT WEAKER_STRIP_TAC;
 709   FIRST_X_ASSUM_ST `scs_generic` MP_TAC;
 710   REWRITE_TAC[Appendix.scs_generic];
 711   DISCH_TAC;
 712   TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
 713   TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
 714   TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
 715   TYPIFY `convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 716     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)`]);
 717   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 718     MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
 719     BY(ASM_REWRITE_TAC[]);
 720   TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
 721     GEN_TAC;
 722     EXPAND_TAC "V";
 723     MATCH_MP_TAC FUN_IN_IMAGE;
 724     BY(REWRITE_TAC[IN_UNIV]);
 725   BY(ASM_MESON_TAC[Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN])
 726   ]);;
 727   (* }}} *)
 728
 729 let coplanar_cross_reduction = prove_by_refinement(
 730   `!s k v i.
 731     is_scs_v39 s /\ scs_k_v39 s = k /\
 732       3 < k /\
 733          MMs_v39 s v /\
 734       scs_basic_v39 s /\
 735          scs_generic v /\
 736          coplanar {vec 0,v i, v(i+1),v(i+2)} ==>
 737          (v(i+1) cross v i) dot (v(i+2) cross v i) > &0`,
 738   (* {{{ proof *)
 739   [
 740   REPEAT WEAKER_STRIP_TAC;
 741   TYPIFY `~(k=0)` (C SUBGOAL_THEN ASSUME_TAC);
 742     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
 743   TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
 744   TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
 745   TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
 746   FIRST_ASSUM_ST `coplanar` MP_TAC;
 747   REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
 748   DISCH_TAC;
 749   TYPIFY `~coplanar ({vec 0} UNION V)` (C SUBGOAL_THEN ASSUME_TAC);
 750     EXPAND_TAC "V";
 751     MATCH_MP_TAC Fektyiy.FEKTYIY;
 752     TYPIFY `s` EXISTS_TAC;
 753     BY(ASM_REWRITE_TAC[IN]);
 754   TYPIFY `BBprime2_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
 755     BY(ASM_MESON_TAC[Appendix.scs_basic;Ayqjtmd.unadorned_MMs]);
 756   TYPIFY `BBprime_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
 757     BY(ASM_MESON_TAC[Appendix.BBprime2_v39]);
 758   TYPIFY `BBs_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
 759     BY(ASM_MESON_TAC[Appendix.BBprime_v39]);
 760   INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`k`];
 761   ASM_REWRITE_TAC[];
 762   DISCH_TAC;
 763   TYPIFY `periodic v k /\ convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 764     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)`]);
 765   INTRO_TAC Terminal.ITER_vv_rho_node1 [`v`;`k`];
 766   ASM_REWRITE_TAC[LET_THM];
 767   ASM_SIMP_TAC[arith `3 < k ==> 3 <= k`];
 768   DISCH_TAC;
 769   INTRO_TAC (GEN_ALL Odxlstcv2.CARD_V_EQ_SCS_K1) [`s`;`v`;`V`;`k`];
 770   ASM_REWRITE_TAC[];
 771   DISCH_TAC;
 772   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 773     MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
 774     BY(ASM_REWRITE_TAC[]);
 775   TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
 776     GEN_TAC;
 777     EXPAND_TAC "V";
 778     MATCH_MP_TAC FUN_IN_IMAGE;
 779     BY(REWRITE_TAC[IN_UNIV]);
 780   TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0, v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
 781     INTRO_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN [`V`;`E`;`FF`];
 782     BY(ASM_MESON_TAC[Appendix.scs_generic]);
 783   INTRO_TAC EGHNAVX_SCS [`s`;`k`;`v`;`i`];
 784   REWRITE_TAC[LET_THM];
 785   ASM_REWRITE_TAC[];
 786   REPEAT WEAKER_STRIP_TAC;
 787   COMMENT "insert here";
 788   TYPIFY `!a. 0 < a /\ (a:num) < k ==> ~(v i = v (i+a))` (C SUBGOAL_THEN ASSUME_TAC);
 789     TYPIFY `!i. v (i MOD k) = v i` (C SUBGOAL_THEN ASSUME_TAC);
 790       GEN_TAC;
 791       MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
 792       BY(ASM_MESON_TAC[arith `3 < k ==> ~(0=k)`]);
 793     FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
 794     GEN_TAC THEN DISCH_TAC;
 795     TYPIFY_GOAL_THEN `!i j. i < k /\ j < (k:num) /\ ~(i = j) ==> ~(v i = v j)` MATCH_MP_TAC;
 796       BY(ASM_MESON_TAC[]);
 797     REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC;
 798       BY(ASM_MESON_TAC[DIVISION]);
 799     TYPIFY `i MOD k = (i+0) MOD k` (C SUBGOAL_THEN SUBST1_TAC);
 800       BY(REWRITE_TAC[arith `i + 0 = i`]);
 801     GMATCH_SIMP_TAC Ocbicby.MOD_EQ_MOD_SHIFT;
 802     REPEAT (GMATCH_SIMP_TAC MOD_LT);
 803     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
 804   FIRST_X_ASSUM DISJ_CASES_TAC;
 805     FIRST_X_ASSUM_ST `&0` (C INTRO_TAC [`2`;`2`]);
 806     ASM_REWRITE_TAC[arith `0 < 2 /\ 2 <= 2 /\ ~(2 < 2)`];
 807     ANTS_TAC;
 808       BY(MATCH_MP_TAC (arith `3 < k ==> 2 < k`) THEN ASM_REWRITE_TAC[]);
 809     GMATCH_SIMP_TAC Local_lemmas1.COLL_AFF_GT_2_1;
 810     SUBCONJ_TAC;
 811       FIRST_X_ASSUM MATCH_MP_TAC;
 812       FIRST_X_ASSUM MATCH_MP_TAC;
 813       BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
 814     DISCH_TAC;
 815     REWRITE_TAC[IN_ELIM_THM];
 816     REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[CROSS_LMUL;CROSS_LADD;DOT_RMUL;DOT_RADD;CROSS_LZERO;DOT_RZERO;CROSS_REFL];
 817     REWRITE_TAC[arith `t1 * &0 + x = x`;arith `x > &0 <=> &0 < x`];
 818     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 819     ASM_REWRITE_TAC[];
 820     REWRITE_TAC[DOT_POS_LT];
 821     REWRITE_TAC[CROSS_EQ_0];
 822     ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
 823     BY(ASM_REWRITE_TAC[]);
 824   COMMENT "second conj";
 825   FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`2`]);
 826   FIRST_X_ASSUM_ST `aff_gt` kill;
 827   FIRST_X_ASSUM_ST `0 < a` MP_TAC THEN BURY_MP_TAC;
 828   FIRST_X_ASSUM (C INTRO_TAC [`2`;`k-1`]);
 829   ANTS_TAC;
 830     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
 831   DISCH_TAC;
 832   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);
 833     BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
 834   DISCH_TAC;
 835   PROOF_BY_CONTR_TAC;
 836   TYPIFY `V SUBSET affine hull {vec 0,v i,v (i+k-1)}` ENOUGH_TO_SHOW_TAC;
 837     DISCH_TAC THEN FIRST_X_ASSUM_ST `coplanar` MP_TAC THEN REWRITE_TAC[coplanar];
 838     GEXISTL_TAC [`(vec 0):real^3`;`v i`;`v (i+k-1)`];
 839     FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_UNION;IN_SING];
 840     TYPIFY `vec 0 IN affine hull {vec 0,v i ,v(i+k-1)}` ENOUGH_TO_SHOW_TAC;
 841       BY(MESON_TAC[]);
 842     MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
 843     BY(SET_TAC[]);
 844   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;
 845     GMATCH_SIMP_TAC (GSYM Oxl_2012.PERIODIC_IMAGE_EQUAL);
 846     ASM_REWRITE_TAC[];
 847     DISCH_TAC;
 848     INTRO_TAC Oxl_def.periodic_numseg [`(\j. v j IN affine hull {vec 0,v i,v (i+k-1)})`;`k`];
 849     ASM_REWRITE_TAC[];
 850     ANTS_TAC;
 851       CONJ_TAC;
 852         FIRST_X_ASSUM_ST `periodic` MP_TAC THEN REWRITE_TAC[Oxl_def.periodic];
 853         BY(MESON_TAC[]);
 854       REPEAT WEAKER_STRIP_TAC;
 855       FIRST_X_ASSUM MATCH_MP_TAC;
 856       MATCH_MP_TAC FUN_IN_IMAGE;
 857       BY(ASM_REWRITE_TAC[]);
 858     DISCH_TAC;
 859     EXPAND_TAC "V";
 860     REWRITE_TAC[IMAGE;IN_UNIV;SUBSET;IN_ELIM_THM];
 861     BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
 862   REWRITE_TAC[IN_IMAGE;IN_NUMSEG];
 863   REPEAT WEAKER_STRIP_TAC;
 864   ASM_REWRITE_TAC[];
 865   TYPIFY `?j. 0 <= j /\ j < k /\ x = i + j` (C SUBGOAL_THEN MP_TAC);
 866     TYPIFY `x - (i:num)` EXISTS_TAC;
 867     BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
 868   REPEAT WEAKER_STRIP_TAC;
 869   ASM_REWRITE_TAC[];
 870   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);
 871     REPEAT WEAKER_STRIP_TAC;
 872     FIRST_X_ASSUM (C INTRO_TAC [`j'`]);
 873     ANTS_TAC;
 874       BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 875     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;
 876       BY(SET_TAC[]);
 877     TYPIFY `{vec 0,v i,v (i+k-1)} = {vec 0,v i} UNION {v (i+k-1)}` (C SUBGOAL_THEN SUBST1_TAC);
 878       BY(SET_TAC[]);
 879     BY(REWRITE_TAC[ AFF_GT_SUBSET_AFFINE_HULL]);
 880   TYPIFY `{vec 0,v i, v (i+2)} SUBSET affine hull {vec 0, v i, v (i+k-1)}` (C SUBGOAL_THEN ASSUME_TAC);
 881     REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
 882     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
 883         MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
 884         BY(SET_TAC[]);
 885       MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
 886       BY(SET_TAC[]);
 887     FIRST_X_ASSUM MATCH_MP_TAC;
 888     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
 889   INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`(vec 0):real^3`;`v i`;`v (i+k-1)`];
 890   ANTS_TAC;
 891     ASM_REWRITE_TAC[];
 892     FIRST_X_ASSUM MATCH_MP_TAC;
 893     FIRST_X_ASSUM MATCH_MP_TAC;
 894     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
 895   DISCH_TAC;
 896   ASSUME_TAC (arith ` 2 <= j \/ j = 0 \/ j = 1` );
 897   REPEAT (POP_ASSUM DISJ_CASES_TAC);
 898       BY(ASM_MESON_TAC[]);
 899     ASM_REWRITE_TAC[arith `i + 0 = i`] THEN MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
 900     BY(SET_TAC[]);
 901   ASM_REWRITE_TAC[];
 902   (FIRST_X_ASSUM_ST `coplanar (a INSERT X)` MP_TAC);
 903   REWRITE_TAC[coplanar] THEN REPEAT WEAKER_STRIP_TAC;
 904   INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`u`;`v'`;`w'`];
 905   ANTS_TAC;
 906     CONJ_TAC;
 907       BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
 908     FIRST_X_ASSUM MATCH_MP_TAC;
 909     FIRST_X_ASSUM MATCH_MP_TAC;
 910     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
 911   BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[])
 912   ]);;
 913   (* }}} *)
 914
 915 let coplanar_aff_gt_simple = prove_by_refinement(
 916   `!s k v i.
 917     is_scs_v39 s /\ scs_k_v39 s = k /\
 918       3 < k /\
 919          MMs_v39 s v /\
 920       scs_basic_v39 s /\
 921         (!j. ~(v j = v i) ==> ~collinear {vec 0,v i,v j}) /\
 922          coplanar {vec 0,v i, v(i+1),v(i+2)} ==>
 923       v (i+1) IN aff_gt {vec 0} {v i, v(i+2)}`,
 924   (* {{{ proof *)
 925   [
 926   REPEAT WEAKER_STRIP_TAC;
 927   TYPIFY `~(k=0)` (C SUBGOAL_THEN ASSUME_TAC);
 928     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
 929   TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
 930   TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
 931   TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
 932   FIRST_ASSUM_ST `coplanar` MP_TAC;
 933   REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
 934   DISCH_TAC;
 935   TYPIFY `~coplanar ({vec 0} UNION V)` (C SUBGOAL_THEN ASSUME_TAC);
 936     EXPAND_TAC "V";
 937     MATCH_MP_TAC Fektyiy.FEKTYIY;
 938     TYPIFY `s` EXISTS_TAC;
 939     BY(ASM_REWRITE_TAC[IN]);
 940   TYPIFY `BBprime2_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
 941     BY(ASM_MESON_TAC[Appendix.scs_basic;Ayqjtmd.unadorned_MMs]);
 942   TYPIFY `BBprime_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
 943     BY(ASM_MESON_TAC[Appendix.BBprime2_v39]);
 944   TYPIFY `BBs_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
 945     BY(ASM_MESON_TAC[Appendix.BBprime_v39]);
 946   INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`k`];
 947   ASM_REWRITE_TAC[];
 948   DISCH_TAC;
 949   TYPIFY `periodic v k /\ convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 950     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)`]);
 951   INTRO_TAC Terminal.ITER_vv_rho_node1 [`v`;`k`];
 952   ASM_REWRITE_TAC[LET_THM];
 953   ASM_SIMP_TAC[arith `3 < k ==> 3 <= k`];
 954   DISCH_TAC;
 955   INTRO_TAC (GEN_ALL Odxlstcv2.CARD_V_EQ_SCS_K1) [`s`;`v`;`V`;`k`];
 956   ASM_REWRITE_TAC[];
 957   DISCH_TAC;
 958   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 959     MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
 960     BY(ASM_REWRITE_TAC[]);
 961   TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
 962     GEN_TAC;
 963     EXPAND_TAC "V";
 964     MATCH_MP_TAC FUN_IN_IMAGE;
 965     BY(REWRITE_TAC[IN_UNIV]);
 966   INTRO_TAC EGHNAVX_COLL_SCS [`s`;`k`;`v`;`i`];
 967   REWRITE_TAC[LET_THM];
 968   ASM_REWRITE_TAC[];
 969   REPEAT WEAKER_STRIP_TAC;
 970   TYPIFY `!a. 0 < a /\ (a:num) < k ==> ~(v i = v (i+a))` (C SUBGOAL_THEN ASSUME_TAC);
 971     TYPIFY `!i. v (i MOD k) = v i` (C SUBGOAL_THEN ASSUME_TAC);
 972       GEN_TAC;
 973       MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
 974       BY(ASM_MESON_TAC[arith `3 < k ==> ~(0=k)`]);
 975     FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
 976     GEN_TAC THEN DISCH_TAC;
 977     TYPIFY_GOAL_THEN `!i j. i < k /\ j < (k:num) /\ ~(i = j) ==> ~(v i = v j)` MATCH_MP_TAC;
 978       BY(ASM_MESON_TAC[]);
 979     REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC;
 980       BY(ASM_MESON_TAC[DIVISION]);
 981     TYPIFY `i MOD k = (i+0) MOD k` (C SUBGOAL_THEN SUBST1_TAC);
 982       BY(REWRITE_TAC[arith `i + 0 = i`]);
 983     GMATCH_SIMP_TAC Ocbicby.MOD_EQ_MOD_SHIFT;
 984     REPEAT (GMATCH_SIMP_TAC MOD_LT);
 985     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
 986   FIRST_X_ASSUM DISJ_CASES_TAC;
 987     FIRST_X_ASSUM_ST `&0` (C INTRO_TAC [`2`;`2`]);
 988     NUM_REDUCE_TAC;
 989     ANTS_TAC;
 990       ASM_REWRITE_TAC[];
 991       BY(MATCH_MP_TAC (arith `3 < k ==> 2 < k`) THEN ASM_REWRITE_TAC[]);
 992     GMATCH_SIMP_TAC Local_lemmas1.COLL_AFF_GT_2_1;
 993     GMATCH_SIMP_TAC AFF_GT_1_2;
 994     REWRITE_TAC[IN_ELIM_THM;arith `t % vec 0 + a = a`];
 995     SUBCONJ_TAC;
 996       ONCE_REWRITE_TAC[DISJOINT_SYM];
 997       MATCH_MP_TAC Fan.th3a;
 998       ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,a,b}`] THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC);
 999       ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN FIRST_X_ASSUM MATCH_MP_TAC;
1000       BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1001     DISCH_TAC;
1002     CONJ_TAC;
1003       FIRST_X_ASSUM MATCH_MP_TAC;
1004       ONCE_REWRITE_TAC[EQ_SYM_EQ];
1005       FIRST_X_ASSUM MATCH_MP_TAC;
1006       BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1007     REPEAT WEAKER_STRIP_TAC;
1008     GEXISTL_TAC [`&1 + t2 / t3 - &1 / t3`;`-- t2 / t3`;`&1 / t3`];
1009     ASM_REWRITE_TAC[];
1010     GMATCH_SIMP_TAC REAL_LT_DIV;
1011     GMATCH_SIMP_TAC REAL_LT_DIV;
1012     ASM_REWRITE_TAC[arith `&0 < &1`];
1013     nCONJ_TAC 2;
1014       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);
1015         BY(VECTOR_ARITH_TAC);
1016       TYPIFY_GOAL_THEN `(--t2 / t3 + &1 / t3 * t2) = &0 /\ (&1 / t3 * t3 = &1)` (unlist REWRITE_TAC);
1017         BY(CONJ_TAC THEN Calc_derivative.CALC_ID_TAC THEN (REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC)) THEN REAL_ARITH_TAC);
1018       BY(VECTOR_ARITH_TAC);
1019     nCONJ_TAC 1;
1020       BY(Calc_derivative.CALC_ID_TAC THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1021     TYPIFY `~(&0 <= t2)` ENOUGH_TO_SHOW_TAC;
1022       BY(REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN MESON_TAC[arith `~(&0 <= t2) ==> &0 < -- t2`]);
1023     DISCH_TAC;
1024     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)`];
1025     ANTS_TAC;
1026       CONJ_TAC;
1027         MATCH_MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
1028         BY(ASM_REWRITE_TAC[]);
1029       CONJ_TAC;
1030         EXPAND_TAC "V";
1031         MATCH_MP_TAC FUN_IN_IMAGE;
1032         BY(REWRITE_TAC[IN_UNIV]);
1033       CONJ_TAC;
1034         EXPAND_TAC "E";
1035         BY(REWRITE_TAC[arith `i+1 = SUC i`;IN_IMAGE;IN_UNIV] THEN MESON_TAC[]);
1036       GMATCH_SIMP_TAC AFF_GE_1_2;
1037       REWRITE_TAC[IN_ELIM_THM];
1038       CONJ_TAC;
1039         ONCE_REWRITE_TAC[DISJOINT_SYM];
1040         MATCH_MP_TAC Fan.th3a;
1041         ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,a,b}`] THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC);
1042         ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN FIRST_X_ASSUM MATCH_MP_TAC;
1043         BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1044       GEXISTL_TAC [`t1`;`t2`;`t3`];
1045       FIRST_X_ASSUM_ST `i+2` SUBST1_TAC;
1046       REWRITE_TAC[CONJ_ASSOC] THEN CONJ2_TAC;
1047         BY(VECTOR_ARITH_TAC);
1048       BY(REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1049     REWRITE_TAC[DE_MORGAN_THM];
1050     CONJ_TAC;
1051       ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN FIRST_X_ASSUM MATCH_MP_TAC;
1052       BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1053     ONCE_REWRITE_TAC[EQ_SYM_EQ];
1054     MATCH_MP_TAC Hypermap_iso.fan_in_e_imp_neq;
1055     GEXISTL_TAC [`V`;`E`];
1056     CONJ_TAC;
1057       MATCH_MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
1058       BY(ASM_REWRITE_TAC[]);
1059     EXPAND_TAC "E";
1060     BY(REWRITE_TAC[arith `i+2 = SUC (i+1)`;IN_IMAGE;IN_UNIV] THEN MESON_TAC[]);
1061   COMMENT "second disj";
1062   FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`2`]);
1063   FIRST_X_ASSUM_ST `aff_gt` kill;
1064   FIRST_X_ASSUM_ST `0 < a` MP_TAC THEN BURY_MP_TAC;
1065   FIRST_X_ASSUM (C INTRO_TAC [`2`;`k-1`]);
1066   ANTS_TAC;
1067     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1068   DISCH_TAC;
1069   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);
1070     BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1071   DISCH_TAC;
1072   PROOF_BY_CONTR_TAC;
1073   TYPIFY `V SUBSET affine hull {vec 0,v i,v (i+k-1)}` ENOUGH_TO_SHOW_TAC;
1074     DISCH_TAC THEN FIRST_X_ASSUM_ST `coplanar` MP_TAC THEN REWRITE_TAC[coplanar];
1075     GEXISTL_TAC [`(vec 0):real^3`;`v i`;`v (i+k-1)`];
1076     FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_UNION;IN_SING];
1077     TYPIFY `vec 0 IN affine hull {vec 0,v i ,v(i+k-1)}` ENOUGH_TO_SHOW_TAC;
1078       BY(MESON_TAC[]);
1079     MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
1080     BY(SET_TAC[]);
1081   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;
1082     GMATCH_SIMP_TAC (GSYM Oxl_2012.PERIODIC_IMAGE_EQUAL);
1083     ASM_REWRITE_TAC[];
1084     DISCH_TAC;
1085     INTRO_TAC Oxl_def.periodic_numseg [`(\j. v j IN affine hull {vec 0,v i,v (i+k-1)})`;`k`];
1086     ASM_REWRITE_TAC[];
1087     ANTS_TAC;
1088       CONJ_TAC;
1089         FIRST_X_ASSUM_ST `periodic` MP_TAC THEN REWRITE_TAC[Oxl_def.periodic];
1090         BY(MESON_TAC[]);
1091       REPEAT WEAKER_STRIP_TAC;
1092       FIRST_X_ASSUM MATCH_MP_TAC;
1093       MATCH_MP_TAC FUN_IN_IMAGE;
1094       BY(ASM_REWRITE_TAC[]);
1095     DISCH_TAC;
1096     EXPAND_TAC "V";
1097     REWRITE_TAC[IMAGE;IN_UNIV;SUBSET;IN_ELIM_THM];
1098     BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
1099   REWRITE_TAC[IN_IMAGE;IN_NUMSEG];
1100   REPEAT WEAKER_STRIP_TAC;
1101   ASM_REWRITE_TAC[];
1102   TYPIFY `?j. 0 <= j /\ j < k /\ x = i + j` (C SUBGOAL_THEN MP_TAC);
1103     TYPIFY `x - (i:num)` EXISTS_TAC;
1104     BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1105   REPEAT WEAKER_STRIP_TAC;
1106   ASM_REWRITE_TAC[];
1107   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);
1108     REPEAT WEAKER_STRIP_TAC;
1109     FIRST_X_ASSUM (C INTRO_TAC [`j'`]);
1110     ANTS_TAC;
1111       BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
1112     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;
1113       BY(SET_TAC[]);
1114     TYPIFY `{vec 0,v i,v (i+k-1)} = {vec 0,v i} UNION {v (i+k-1)}` (C SUBGOAL_THEN SUBST1_TAC);
1115       BY(SET_TAC[]);
1116     BY(REWRITE_TAC[ AFF_GT_SUBSET_AFFINE_HULL]);
1117   TYPIFY `{vec 0,v i, v (i+2)} SUBSET affine hull {vec 0, v i, v (i+k-1)}` (C SUBGOAL_THEN ASSUME_TAC);
1118     REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
1119     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
1120         MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
1121         BY(SET_TAC[]);
1122       MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
1123       BY(SET_TAC[]);
1124     FIRST_X_ASSUM MATCH_MP_TAC;
1125     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1126   INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`(vec 0):real^3`;`v i`;`v (i+k-1)`];
1127   ANTS_TAC;
1128     ASM_REWRITE_TAC[];
1129     FIRST_X_ASSUM MATCH_MP_TAC;
1130     ONCE_REWRITE_TAC[EQ_SYM_EQ];
1131     FIRST_X_ASSUM MATCH_MP_TAC;
1132     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1133   INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`(vec 0):real^3`;`v i`;`v (i+k-1)`];
1134   ANTS_TAC;
1135     ASM_REWRITE_TAC[];
1136     FIRST_X_ASSUM MATCH_MP_TAC;
1137     ONCE_REWRITE_TAC[EQ_SYM_EQ];
1138     FIRST_X_ASSUM MATCH_MP_TAC;
1139     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1140   DISCH_TAC;
1141   ASSUME_TAC (arith ` 2 <= j \/ j = 0 \/ j = 1` );
1142   REPEAT (POP_ASSUM DISJ_CASES_TAC);
1143       BY(ASM_MESON_TAC[]);
1144     ASM_REWRITE_TAC[arith `i + 0 = i`] THEN MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
1145     BY(SET_TAC[]);
1146   ASM_REWRITE_TAC[];
1147   (FIRST_X_ASSUM_ST `coplanar (a INSERT X)` MP_TAC);
1148   REWRITE_TAC[coplanar] THEN REPEAT WEAKER_STRIP_TAC;
1149   INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`u`;`v'`;`w'`];
1150   ANTS_TAC;
1151     CONJ_TAC;
1152       BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
1153     FIRST_X_ASSUM MATCH_MP_TAC;
1154     ONCE_REWRITE_TAC[EQ_SYM_EQ];
1155     FIRST_X_ASSUM MATCH_MP_TAC;
1156     BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1157   BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[])
1158   ]);;
1159   (* }}} *)
1160
1161 (*
1162 let a5_assumption_reduction = prove_by_refinement(
1163   `!s f v e.
1164     is_scs_v39 s /\
1165     scs_k_v39 s  = 5 /\
1166     BBs_v39 s v /\
1167     (!i j. scs_diag 5 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
1168     deformation f (IMAGE v (:num)) (--e,e) /\
1169     (!w t. ~(w = v 0) /\ ~(w = v 1)  ==> (f w t = w)) /\
1170     (?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))) /\
1171     (?e1. &0 < e1 /\ (!t. abs t < e1 ==> scs_a_v39 s 0 1 <= dist(f (v 0) t,f (v 1) t)))
1172     ==>
1173     (!i j. ?e1. &0 < e1 /\ (scs_a_v39 s i j = dist(v i,v j) ==>
1174         (!t. abs t < e1 ==> scs_a_v39 s i j <= dist(f (v i) t,f (v j) t))))
1175     `,
1176   (* {{{ proof *)
1177   [
1178   REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC Cuxvzoz.I_IMP THEN ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
1179   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);
1180     FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC;
1181     ASM_REWRITE_TAC[Appendix.is_scs_v39];
1182     REPEAT WEAKER_STRIP_TAC;
1183     BY(REPEAT (FIRST_X_ASSUM_ST `periodic2` MP_TAC) THEN MESON_TAC[Cuxvzoz.periodic2_MOD;arith `~(5 = 0)`]);
1184   TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
1185     BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
1186   TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
1187     GEN_TAC;
1188     MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
1189     BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
1190   INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
1191   ASM_REWRITE_TAC[];
1192   DISCH_TAC;
1193   TYPIFY `!j. j < 5 ==> (j MOD 5 = j)` (C SUBGOAL_THEN ASSUME_TAC);
1194     BY(REWRITE_TAC[MOD_LT]);
1195   COMMENT "scs_a_v39";
1196   REWRITE_TAC[I_THM];
1197   MATCH_MP_TAC Terminal.periodic2_mod_reduce;
1198   TYPIFY `5` EXISTS_TAC;
1199   ASM_REWRITE_TAC[arith `~(5=0)`];
1200   CONJ_TAC;
1201     MATCH_MP_TAC Cuxvzoz.MOD_periodic2;
1202     BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[] THEN MESON_TAC[arith `~(5=0)`]);
1203   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;
1204     BY(MESON_TAC[arith `i <= j \/ j <= (i:num)`]);
1205   CONJ_TAC;
1206     REPEAT WEAKER_STRIP_TAC;
1207     ONCE_REWRITE_TAC[DIST_SYM];
1208     TYPIFY `scs_a_v39 s j i = scs_a_v39 s i j` (C SUBGOAL_THEN SUBST1_TAC);
1209       FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC THEN REWRITE_TAC[Appendix.is_scs_v39] THEN REPEAT WEAKER_STRIP_TAC;
1210       BY(ASM_MESON_TAC[]);
1211     FIRST_X_ASSUM MATCH_MP_TAC;
1212     BY(ASM_REWRITE_TAC[]);
1213   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);
1214     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)`]);
1215   REWRITE_TAC[arith `i < 5 <=> (i = 0) \/ (i = 1) \/ (i=2) \/ (i  =3) \/ (i=4)`];
1216   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);
1217     BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
1218   ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
1219   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);
1220     BY(ASM_MESON_TAC[arith `x < y ==> ~(x = y)`]);
1221   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);
1222     REWRITE_TAC[DIST_REFL];
1223     BY(MESON_TAC[arith `x = &0 ==> x <= &0`;arith `&0 < &1`]);
1224   REPEAT GEN_TAC;
1225   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);
1226     ASM_REWRITE_TAC[];
1227     TYPIFY_GOAL_THEN `!a b. (?e1. &0 < e1 /\ (a = b ==> (!t. abs t < e1 ==> a <= b)))` (unlist REWRITE_TAC);
1228       BY(MESON_TAC[arith `&0 < &1`;arith `(a = b) ==> (a <= b)`]);
1229     CONJ_TAC;
1230       BY(ASM_MESON_TAC[]);
1231     BY(ASM_MESON_TAC[arith `x = y ==> x <= y`]);
1232   REWRITE_TAC[LEFT_OR_DISTRIB;RIGHT_OR_DISTRIB;GSYM DISJ_ASSOC];
1233   ONCE_REWRITE_TAC[TAUT `(a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ((T ==> a1) /\ (T ==> a2) /\ (T ==> a3) /\ (T ==> a4) /\ (T ==> a5))`];
1234   REPEAT WEAKER_STRIP_TAC;
1235   FIRST_X_ASSUM MP_TAC;
1236   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[])
1237   ]);;
1238   (* }}} *)
1239 *)
1240
1241 let a5_assumption_reduction = prove_by_refinement(
1242   `!s f v e.
1243     is_scs_v39 s /\
1244     scs_k_v39 s  = 5 /\
1245     BBs_v39 s v /\
1246     (!i j. scs_diag 5 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
1247     deformation f (IMAGE v (:num)) (--e,e) /\
1248     (!w t. ~(w = v 4) /\ ~(w = v 0)  ==> (f w t = w)) /\
1249     (?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))) /\
1250     (?e1. &0 < e1 /\ (!t. abs t < e1 ==> scs_a_v39 s 0 1 <= dist(f (v 0) t,v 1)))
1251     ==>
1252     (!i j. ?e1. &0 < e1 /\ (scs_a_v39 s i j = dist(v i,v j) ==>
1253         (!t. abs t < e1 ==> scs_a_v39 s i j <= dist(f (v i) t,f (v j) t))))
1254     `,
1255   (* {{{ proof *)
1256   [
1257   REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC Cuxvzoz.I_IMP THEN ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
1258   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);
1259     FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC;
1260     ASM_REWRITE_TAC[Appendix.is_scs_v39];
1261     REPEAT WEAKER_STRIP_TAC;
1262     BY(REPEAT (FIRST_X_ASSUM_ST `periodic2` MP_TAC) THEN MESON_TAC[Cuxvzoz.periodic2_MOD;arith `~(5 = 0)`]);
1263   TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
1264     BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
1265   TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
1266     GEN_TAC;
1267     MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
1268     BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
1269   INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
1270   ASM_REWRITE_TAC[];
1271   DISCH_TAC;
1272   TYPIFY `!j. j < 5 ==> (j MOD 5 = j)` (C SUBGOAL_THEN ASSUME_TAC);
1273     BY(REWRITE_TAC[MOD_LT]);
1274   COMMENT "scs_a_v39";
1275   REWRITE_TAC[I_THM];
1276   MATCH_MP_TAC Terminal.periodic2_mod_reduce;
1277   TYPIFY `5` EXISTS_TAC;
1278   ASM_REWRITE_TAC[arith `~(5=0)`];
1279   CONJ_TAC;
1280     MATCH_MP_TAC Cuxvzoz.MOD_periodic2;
1281     BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[] THEN MESON_TAC[arith `~(5=0)`]);
1282   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;
1283     BY(MESON_TAC[arith `i <= j \/ j <= (i:num)`]);
1284   CONJ_TAC;
1285     REPEAT WEAKER_STRIP_TAC;
1286     ONCE_REWRITE_TAC[DIST_SYM];
1287     TYPIFY `scs_a_v39 s j i = scs_a_v39 s i j` (C SUBGOAL_THEN SUBST1_TAC);
1288       FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC THEN REWRITE_TAC[Appendix.is_scs_v39] THEN REPEAT WEAKER_STRIP_TAC;
1289       BY(ASM_MESON_TAC[]);
1290     FIRST_X_ASSUM MATCH_MP_TAC;
1291     BY(ASM_REWRITE_TAC[]);
1292   TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i=j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
1293     BY(ASM_MESON_TAC[]);
1294   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);
1295     BY(GEN_TAC THEN REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC) THEN NUM_REDUCE_TAC);
1296   REWRITE_TAC[arith `i < 5 <=> (i = 0) \/ (i = 1) \/ (i=2) \/ (i  =3) \/ (i=4)`];
1297   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);
1298     BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
1299   ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
1300   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);
1301     BY(ASM_MESON_TAC[arith `x < y ==> ~(x = y)`]);
1302   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);
1303     REWRITE_TAC[DIST_REFL];
1304     BY(MESON_TAC[arith `x = &0 ==> x <= &0`;arith `&0 < &1`]);
1305   REPEAT GEN_TAC;
1306   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);
1307     ASM_REWRITE_TAC[];
1308     TYPIFY_GOAL_THEN `!a b. (?e1. &0 < e1 /\ (a = b ==> (!t. abs t < e1 ==> a <= b)))` (unlist REWRITE_TAC);
1309       BY(MESON_TAC[arith `&0 < &1`;arith `(a = b) ==> (a <= b)`]);
1310     CONJ_TAC;
1311       BY(ASM_MESON_TAC[]);
1312     ONCE_REWRITE_TAC[DIST_SYM];
1313     BY(ASM_MESON_TAC[arith `x = y ==> x <= y`]);
1314   REWRITE_TAC[LEFT_OR_DISTRIB;RIGHT_OR_DISTRIB;GSYM DISJ_ASSOC];
1315   ONCE_REWRITE_TAC[TAUT `(a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ((T ==> a1) /\ (T ==> a2) /\ (T ==> a3) /\ (T ==> a4) /\ (T ==> a5))`];
1316   REPEAT WEAKER_STRIP_TAC;
1317   FIRST_X_ASSUM MP_TAC;
1318   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[])
1319   ]);;
1320   (* }}} *)
1321
1322 (*
1323 let b5_assumption_reduction = prove_by_refinement(
1324   `!s f v e.
1325     is_scs_v39 s /\
1326     scs_k_v39 s  = 5 /\
1327     BBs_v39 s v /\
1328     (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 s i j) /\
1329     deformation f (IMAGE v (:num)) (--e,e) /\
1330     (!w t. ~(w = v 0) /\ ~(w = v 1)  ==> (f w t = w)) /\
1331     (?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))) /\
1332     (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 0) t,f (v 1) t) <= dist(v 0, v 1)))
1333     ==>
1334     (!i j. ?e1. &0 < e1 /\ (dist(v i,v j) = scs_b_v39 s i j ==>
1335         (!t. abs t < e1 ==> dist(f (v i) t,f (v j) t) <= scs_b_v39 s i j)))
1336     `,
1337   (* {{{ proof *)
1338   [
1339   REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC Cuxvzoz.I_IMP THEN ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
1340   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);
1341     FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC;
1342     ASM_REWRITE_TAC[Appendix.is_scs_v39];
1343     REPEAT WEAKER_STRIP_TAC;
1344     BY(REPEAT (FIRST_X_ASSUM_ST `periodic2` MP_TAC) THEN MESON_TAC[Cuxvzoz.periodic2_MOD;arith `~(5 = 0)`]);
1345   TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
1346     BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
1347   TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
1348     GEN_TAC;
1349     MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
1350     BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
1351   INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
1352   ASM_REWRITE_TAC[];
1353   DISCH_TAC;
1354   TYPIFY `!j. j < 5 ==> (j MOD 5 = j)` (C SUBGOAL_THEN ASSUME_TAC);
1355     BY(REWRITE_TAC[MOD_LT]);
1356   COMMENT "scs_b_v39";
1357   REWRITE_TAC[I_THM];
1358   MATCH_MP_TAC Terminal.periodic2_mod_reduce;
1359   TYPIFY `5` EXISTS_TAC;
1360   ASM_REWRITE_TAC[arith `~(5=0)`];
1361   CONJ_TAC;
1362     MATCH_MP_TAC Cuxvzoz.MOD_periodic2;
1363     BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[] THEN MESON_TAC[arith `~(5=0)`]);
1364   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;
1365     BY(MESON_TAC[arith `i <= j \/ j <= (i:num)`]);
1366   CONJ_TAC;
1367     REPEAT WEAKER_STRIP_TAC;
1368     ONCE_REWRITE_TAC[DIST_SYM];
1369     TYPIFY `scs_b_v39 s j i = scs_b_v39 s i j` (C SUBGOAL_THEN SUBST1_TAC);
1370       FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC THEN REWRITE_TAC[Appendix.is_scs_v39] THEN REPEAT WEAKER_STRIP_TAC;
1371       BY(ASM_MESON_TAC[]);
1372     FIRST_X_ASSUM MATCH_MP_TAC;
1373     BY(ASM_REWRITE_TAC[]);
1374   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);
1375     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)`]);
1376   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);
1377     BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
1378   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);
1379     REPEAT WEAKER_STRIP_TAC;
1380     TYPIFY `&1` EXISTS_TAC;
1381     (REWRITE_TAC[arith `&0 < &1`]);
1382     TYPIFY `dist(v i,v j) <= &4 * h0` ENOUGH_TO_SHOW_TAC;
1383       FIRST_X_ASSUM_ST `&4 * h0` (C INTRO_TAC [`i`;`j`]);
1384       ASM_REWRITE_TAC[];
1385       BY(REAL_ARITH_TAC);
1386     INTRO_TAC DIST_TRIANGLE [`v i`;`(vec 0):real^3`;`v j`];
1387     REWRITE_TAC[DIST_0];
1388     TYPIFY `!i. norm (v i) <= &2 * h0` ENOUGH_TO_SHOW_TAC;
1389       BY(DISCH_TAC THEN FIRST_ASSUM (C INTRO_TAC [`i`]) THEN FIRST_X_ASSUM (C INTRO_TAC [`j`]) THEN REAL_ARITH_TAC);
1390     FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN REPEAT WEAKER_STRIP_TAC;
1391     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]);
1392   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);
1393     REWRITE_TAC[DIST_REFL];
1394     BY(MESON_TAC[arith `x = &0 ==> x <= &0`;arith `&0 < &1`]);
1395   REPEAT GEN_TAC;
1396   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);
1397     ASM_REWRITE_TAC[];
1398     TYPIFY_GOAL_THEN `!a b. (?e1. &0 < e1 /\ (a = b ==> (!t. abs t < e1 ==> a <= b)))` (unlist REWRITE_TAC);
1399       BY(MESON_TAC[arith `&0 < &1`;arith `(a = b) ==> (a <= b)`]);
1400     CONJ_TAC;
1401       BY(ASM_MESON_TAC[]);
1402     BY(ASM_MESON_TAC[arith `x = y ==> x <= y`]);
1403   DISCH_TAC;
1404   REWRITE_TAC[arith `i < 5 <=> (i = 0) \/ (i = 1) \/ (i=2) \/ (i  =3) \/ (i=4)`];
1405   ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
1406   REWRITE_TAC[LEFT_OR_DISTRIB;RIGHT_OR_DISTRIB;GSYM DISJ_ASSOC];
1407   FIRST_X_ASSUM MP_TAC;
1408   ONCE_REWRITE_TAC[TAUT `(a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ((T ==> a1) /\ (T ==> a2) /\ (T ==> a3) /\ (T ==> a4) /\ (T ==> a5))`];
1409   REPEAT WEAKER_STRIP_TAC;
1410   FIRST_X_ASSUM MP_TAC;
1411   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[])
1412   ]);;
1413   (* }}} *)
1414 *)
1415
1416 let b5_assumption_reduction = prove_by_refinement(
1417   `!s f v e.
1418     is_scs_v39 s /\
1419     scs_k_v39 s  = 5 /\
1420     BBs_v39 s v /\
1421     (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 s i j) /\
1422     deformation f (IMAGE v (:num)) (--e,e) /\
1423     (!w t. ~(w = v 4) /\ ~(w = v 0)  ==> (f w t = w)) /\
1424     (?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))) /\
1425     (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 0) t, (v 1)) <= dist(v 0, v 1)))
1426     ==>
1427     (!i j. ?e1. &0 < e1 /\ (dist(v i,v j) = scs_b_v39 s i j ==>
1428         (!t. abs t < e1 ==> dist(f (v i) t,f (v j) t) <= scs_b_v39 s i j)))
1429     `,
1430   (* {{{ proof *)
1431   [
1432   REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC Cuxvzoz.I_IMP THEN ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
1433   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);
1434     FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC;
1435     ASM_REWRITE_TAC[Appendix.is_scs_v39];
1436     REPEAT WEAKER_STRIP_TAC;
1437     BY(REPEAT (FIRST_X_ASSUM_ST `periodic2` MP_TAC) THEN MESON_TAC[Cuxvzoz.periodic2_MOD;arith `~(5 = 0)`]);
1438   TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
1439     BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
1440   TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
1441     GEN_TAC;
1442     MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
1443     BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
1444   INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
1445   ASM_REWRITE_TAC[];
1446   DISCH_TAC;
1447   TYPIFY `!j. j < 5 ==> (j MOD 5 = j)` (C SUBGOAL_THEN ASSUME_TAC);
1448     BY(REWRITE_TAC[MOD_LT]);
1449   COMMENT "scs_b_v39";
1450   REWRITE_TAC[I_THM];
1451   MATCH_MP_TAC Terminal.periodic2_mod_reduce;
1452   TYPIFY `5` EXISTS_TAC;
1453   ASM_REWRITE_TAC[arith `~(5=0)`];
1454   CONJ_TAC;
1455     MATCH_MP_TAC Cuxvzoz.MOD_periodic2;
1456     BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[] THEN MESON_TAC[arith `~(5=0)`]);
1457   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;
1458     BY(MESON_TAC[arith `i <= j \/ j <= (i:num)`]);
1459   CONJ_TAC;
1460     REPEAT WEAKER_STRIP_TAC;
1461     ONCE_REWRITE_TAC[DIST_SYM];
1462     TYPIFY `scs_b_v39 s j i = scs_b_v39 s i j` (C SUBGOAL_THEN SUBST1_TAC);
1463       FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC THEN REWRITE_TAC[Appendix.is_scs_v39] THEN REPEAT WEAKER_STRIP_TAC;
1464       BY(ASM_MESON_TAC[]);
1465     FIRST_X_ASSUM MATCH_MP_TAC;
1466     BY(ASM_REWRITE_TAC[]);
1467   TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i=j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
1468     BY(ASM_MESON_TAC[]);
1469   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);
1470     BY(GEN_TAC THEN REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC) THEN NUM_REDUCE_TAC);
1471   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);
1472     BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
1473   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);
1474     REPEAT WEAKER_STRIP_TAC;
1475     TYPIFY `&1` EXISTS_TAC;
1476     (REWRITE_TAC[arith `&0 < &1`]);
1477     TYPIFY `dist(v i,v j) <= &4 * h0` ENOUGH_TO_SHOW_TAC;
1478       FIRST_X_ASSUM_ST `&4 * h0` (C INTRO_TAC [`i`;`j`]);
1479       ASM_REWRITE_TAC[];
1480       BY(REAL_ARITH_TAC);
1481     INTRO_TAC DIST_TRIANGLE [`v i`;`(vec 0):real^3`;`v j`];
1482     REWRITE_TAC[DIST_0];
1483     TYPIFY `!i. norm (v i) <= &2 * h0` ENOUGH_TO_SHOW_TAC;
1484       BY(DISCH_TAC THEN FIRST_ASSUM (C INTRO_TAC [`i`]) THEN FIRST_X_ASSUM (C INTRO_TAC [`j`]) THEN REAL_ARITH_TAC);
1485     FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN REPEAT WEAKER_STRIP_TAC;
1486     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]);
1487   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);
1488     REWRITE_TAC[DIST_REFL];
1489     BY(MESON_TAC[arith `x = &0 ==> x <= &0`;arith `&0 < &1`]);
1490   REPEAT GEN_TAC;
1491   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);
1492     ASM_REWRITE_TAC[];
1493     TYPIFY_GOAL_THEN `!a b. (?e1. &0 < e1 /\ (a = b ==> (!t. abs t < e1 ==> a <= b)))` (unlist REWRITE_TAC);
1494       BY(MESON_TAC[arith `&0 < &1`;arith `(a = b) ==> (a <= b)`]);
1495     CONJ_TAC;
1496       BY(ASM_MESON_TAC[]);
1497     REPEAT (FIRST_X_ASSUM_ST `dist(v 4,v 0)` MP_TAC);
1498     REWRITE_TAC[DIST_SYM];
1499     BY(ASM_MESON_TAC[arith `x = y ==> x <= y`]);
1500   DISCH_TAC;
1501   REWRITE_TAC[arith `i < 5 <=> (i = 0) \/ (i = 1) \/ (i=2) \/ (i  =3) \/ (i=4)`];
1502   ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
1503   REWRITE_TAC[LEFT_OR_DISTRIB;RIGHT_OR_DISTRIB;GSYM DISJ_ASSOC];
1504   FIRST_X_ASSUM MP_TAC;
1505   ONCE_REWRITE_TAC[TAUT `(a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ((T ==> a1) /\ (T ==> a2) /\ (T ==> a3) /\ (T ==> a4) /\ (T ==> a5))`];
1506   REPEAT WEAKER_STRIP_TAC;
1507   FIRST_X_ASSUM MP_TAC;
1508   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[])
1509   ]);;
1510   (* }}} *)
1511
1512 (* was dihV_dih_y *)
1513
1514 let azim_dih_y = prove_by_refinement(
1515   `!v0 v1 v2 v3. ~collinear {v0,v1,v2} /\ ~collinear{v0,v1,v3} /\ azim v0 v1 v2 v3 <= pi ==>
1516     azim v0 v1 v2 v3 = dih_y (dist(v0,v1)) (dist(v0,v2)) (dist(v0,v3))
1517       (dist(v2,v3)) (dist(v1,v3)) (dist(v1,v2))`,
1518   (* {{{ proof *)
1519   [
1520   REPEAT WEAKER_STRIP_TAC;
1521   INTRO_TAC AZIM_DIHV_SAME_STRONG [`v0`;`v1`;`v2`;`v3`];
1522   ASM_REWRITE_TAC[];
1523   DISCH_THEN SUBST1_TAC;
1524   GMATCH_SIMP_TAC (REWRITE_RULE[LET_THM] Merge_ineq.DIHV_DIH_X);
1525   REWRITE_TAC[Sphere.dih_y;LET_THM;arith `x*x = x pow 2`];
1526   BY(ASM_REWRITE_TAC[GSYM Collect_geom2.NOT_COL_EQ_UPS_X_POS])
1527   ]);;
1528   (* }}} *)
1529
1530 (* next azim reduction *)
1531
1532 (*
1533 let azm5_reduction = prove_by_refinement(
1534  `!s f v e.
1535      is_scs_v39 s /\
1536      scs_k_v39 s = 5 /\
1537      BBs_v39 s v /\
1538      scs_generic v /\
1539      deformation f (IMAGE v (:num)) (--e,e) /\
1540      (!w t. ~(w = v 0) /\ ~(w = v 4) ==> f w t = w) /\
1541      azim (vec 0) (v 0) (v 1) (v 4) < pi /\
1542      azim (vec 0) (v 1) (v 2) (v 0) < pi /\
1543      &0 < azim (vec 0) (v 0) (v 1) (v 3) /\
1544      (?e1. &0 < e1 /\
1545            (!t. abs t < e1
1546                 ==> azim (vec 0) (v 3) (f (v 0) t) (v 1) <=
1547                     azim (vec 0) (v 3) (v 0) (v 1))) /\
1548      (?e1. &0 < e1 /\
1549            (!t. abs t < e1
1550                   // make this a dih_y condition??
1551                 ==> azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) =
1552                     azim (vec 0) (v 3) (v 4) (v 0) /\
1553                     azim (vec 0) (f (v 4) t) (f (v 0) t) (v 3) =
1554                     azim (vec 0) (v 4) (v 0) (v 3) /\
1555                     azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) =
1556                     azim (vec 0) (v 0) (v 3) (v 4)))
1557      ==> azim (vec 0) (v 3) (v 4) (v 2) =
1558          azim (vec 0) (v 3) (v 4) (v 0) +
1559          azim (vec 0) (v 3) (v 0) (v 1) +
1560          azim (vec 0) (v 3) (v 1) (v 2) /\
1561          azim (vec 0) (v 0) (v 1) (v 4) =
1562          azim (vec 0) (v 0) (v 1) (v 3) + azim (vec 0) (v 0) (v 3) (v 4) /\
1563          azim (vec 0) (v 1) (v 2) (v 0) =
1564          azim (vec 0) (v 1) (v 2) (v 3) + azim (vec 0) (v 1) (v 3) (v 0) /\
1565          (?e1. &0 < e1 /\
1566                (!t. abs t < e1
1567                     ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) =
1568                         azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) +
1569                         azim (vec 0) (v 3) (f (v 0) t) (v 1) +
1570                         azim (vec 0) (v 3) (v 1) (v 2) /\
1571                         azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) =
1572                         azim (vec 0) (f (v 0) t) (v 1) (v 3) +
1573                         azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) /\
1574                         azim (vec 0) (v 1) (v 2) (f (v 0) t) =
1575                         azim (vec 0) (v 1) (v 2) (v 3) +
1576                         azim (vec 0) (v 1) (v 3) (f (v 0) t) /\
1577                         &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\
1578                         azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi)) /\
1579          (!i. ?e0. &0 < e0 /\
1580                    (azim (vec 0) (v i) (v (i + 1)) (v (i + 4)) = pi
1581                     ==> (!t. abs t < e0
1582                              ==> azim (vec 0) (f (v i) t) (f (v (i + 1)) t)
1583                                  (f (v (i + 4)) t) <=
1584                                  pi)))`,
1585   (* {{{ proof *)
1586   [
1587   REPEAT WEAKER_STRIP_TAC;
1588   ASSUME_TAC (arith `~(0 = 5)`);
1589   TYPIFY `!i. i MOD 5 < 5` (C SUBGOAL_THEN ASSUME_TAC);
1590     BY((FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[DIVISION]);
1591   TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
1592     BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
1593   TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
1594     GEN_TAC;
1595     MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
1596     BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
1597   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);
1598     FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
1599     BY(REWRITE_TAC[Ocbicby.MOD_5_EXPLICIT;arith `8 = 1*5 + 3`;arith `9 = 1*5 + 4`;MOD_MULT_ADD]);
1600   INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
1601   ASM_REWRITE_TAC[];
1602   DISCH_TAC;
1603   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);
1604     CONJ2_TAC;
1605       FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[LET_THM;Appendix.BBs_v39];
1606       BY(MESON_TAC[arith `~(5 <= 3)`]);
1607     BY(FIRST_X_ASSUM_ST `scs_generic` MP_TAC THEN MESON_TAC[Appendix.scs_generic]);
1608   FIRST_X_ASSUM MP_TAC THEN BURY_MP_TAC;
1609   COMMENT "first addition";
1610   SUBCONJ_TAC;
1611     INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`3`;`4`];
1612     ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 4 = 7 /\ 3 + 3  = 6 /\ 3 <= 5 /\ 0 < 3 /\ 3 < 4 /\ 4 < 5`];
1613     DISCH_THEN SUBST1_TAC;
1614     INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`2`;`3`];
1615     ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 3 = 6 /\ 3 + 2  = 5 /\ 3 <= 5 /\ 0 < 2 /\ 2 < 3 /\ 3 < 5`];
1616     DISCH_THEN SUBST1_TAC;
1617     BY(REAL_ARITH_TAC);
1618   DISCH_TAC;
1619   COMMENT "second addition";
1620   SUBCONJ_TAC;
1621     INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
1622     NUM_REDUCE_TAC;
1623     BY(ASM_REWRITE_TAC[LET_THM]);
1624   COMMENT "third addition";
1625   INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
1626   NUM_REDUCE_TAC;
1627   ASM_REWRITE_TAC[LET_THM];
1628   DISCH_TAC;
1629   DISCH_TAC;
1630   SUBCONJ_TAC;
1631     INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`1`;`2`;`4`];
1632     NUM_REDUCE_TAC;
1633     BY(ASM_REWRITE_TAC[LET_THM]);
1634   DISCH_TAC;
1635   TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i = j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
1636     BY(ASM_MESON_TAC[]);
1637   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);
1638     GEN_TAC;
1639     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);
1640   COMMENT "colinearity";
1641   TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0,v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
1642     REPEAT GEN_TAC THEN DISCH_TAC;
1643     MATCH_MP_TAC Zlzthic.PROPERTIES_GENERIC_LOCAL_FAN_ALT;
1644     GEXISTL_TAC [`IMAGE v (:num)`;`IMAGE (\i. {v i, v (SUC i)}) (:num)`;`IMAGE (\i. (v i, v (SUC i))) (:num)`];
1645     ASM_REWRITE_TAC[IN_IMAGE;IN_UNIV];
1646     CONJ_TAC;
1647       MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
1648       BY(ASM_REWRITE_TAC[]);
1649     BY(MESON_TAC[]);
1650   COMMENT "deform collinear";
1651   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);
1652     REPEAT WEAKER_STRIP_TAC;
1653     INTRO_TAC (GEN_ALL Local_lemmas1.CONTINUOUS_PRESERVE_COLLINEAR) [`&0`;`(vec 0):real^3`;`f (v i)`;`f (v j)`];
1654     ANTS_TAC;
1655       FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation;arith `abs(&0 - x) = abs x`];
1656       REWRITE_TAC[IN_IMAGE;IN_UNIV];
1657       BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
1658     BY(REWRITE_TAC[arith `abs(&0 - r') = abs r'`]);
1659   TYPIFY `!i. azim (vec 0) (v i) (v (i+1)) (v(i+4)) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
1660     REWRITE_TAC[arith `i+1 = SUC i`;arith `4 = 5 - 1`];
1661     GEN_TAC;
1662     MATCH_MP_TAC (REWRITE_RULE[LET_THM] Terminal.convex_local_fan_azim_le_pi);
1663     ASM_REWRITE_TAC[arith `3 <= 5`];
1664     FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM];
1665     BY(DISCH_THEN (unlist REWRITE_TAC));
1666   COMMENT "merge e";
1667   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);
1668     REPEAT WEAKER_STRIP_TAC;
1669     INTRO_TAC Cuxvzoz.epsilon_quad [`e1''`;`e1'''`;`e1''''`;`e1'''''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1670     TYPIFY `e''''` EXISTS_TAC;
1671     ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC THEN REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[];
1672       BY(ASM_MESON_TAC[]);
1673     BY(ASM_MESON_TAC[]);
1674   REWRITE_TAC[GSYM CONJ_ASSOC];
1675   COMMENT "azim bounds";
1676   TYPIFY `azim (vec 0) (v 0) (v 1) (v 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
1677     FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 4) < pi` MP_TAC;
1678     ASM_REWRITE_TAC[];
1679     MATCH_MP_TAC (arith `&0 <= y ==> (x + y < pi ==> x < pi)`);
1680     BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
1681   TYPIFY `~coplanar {vec 0,v 0,v 1,v 3}` (C SUBGOAL_THEN ASSUME_TAC);
1682     REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
1683     BY(REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 3)` MP_TAC) THEN REAL_ARITH_TAC);
1684   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);
1685     REWRITE_TAC[Zlzthic.azim_pos_iff_nz];
1686     FIRST_X_ASSUM_ST `coplanar` MP_TAC;
1687     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}`]);
1688   INTRO_TAC Cuxvzoz.WNWSHJT_ALT [`v 3`;`v 0`;`v 1`;`f`;`-- e`;`e`;`pi - azim (vec 0) (v 0) (v 3) (v 4)`];
1689   ANTS_TAC;
1690     ASM_REWRITE_TAC[arith `a < pi - b <=> a + b < pi`];
1691     CONJ_TAC;
1692       MATCH_MP_TAC Zlzthic.deformation_subset;
1693       TYPIFY `IMAGE v (:num)` EXISTS_TAC;
1694       ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_UNIV];
1695       BY(MESON_TAC[FUN_IN_IMAGE;IN_UNIV]);
1696     REWRITE_TAC[CONJ_ASSOC];
1697     CONJ_TAC;
1698       FIRST_X_ASSUM_ST `coplanar` MP_TAC;
1699       BY(MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan;SET_RULE `{a,b,c} = {a,c,b}`]);
1700     BY(REPEAT (FIRST_X_ASSUM_ST `x < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1701   REPEAT WEAKER_STRIP_TAC;
1702   INTRO_TAC Cuxvzoz.WNWSHJT_ALT [`v 0`;`v 1`;`v 3`;`f`;`-- e`;`e`;`pi - azim (vec 0) (v 1) (v 2) (v 3)`];
1703   ANTS_TAC;
1704     ASM_REWRITE_TAC[arith `a < pi - b <=> a + b < pi`];
1705     CONJ_TAC;
1706       MATCH_MP_TAC Zlzthic.deformation_subset;
1707       TYPIFY `IMAGE v (:num)` EXISTS_TAC;
1708       ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_UNIV];
1709       BY(MESON_TAC[FUN_IN_IMAGE;IN_UNIV]);
1710     REWRITE_TAC[CONJ_ASSOC];
1711     CONJ_TAC;
1712       FIRST_X_ASSUM_ST `coplanar` MP_TAC;
1713       BY(MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan;SET_RULE `{a,b,c} = {a,c,b}`]);
1714     BY(REPEAT (FIRST_X_ASSUM_ST `x < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1715   REPEAT WEAKER_STRIP_TAC;
1716   COMMENT "azim additivity";
1717   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);
1718     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];
1719     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];
1720     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];
1721     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];
1722     INTRO_TAC Cuxvzoz.epsilon_quad [`e1''`;`e1'''`;`e1''''`;`e1'''''`] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
1723     TYPIFY `e''''` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
1724     BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);
1725   FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
1726   SUBCONJ_TAC;
1727     INTRO_TAC Cuxvzoz.epsilon_triple [`e1`;`e1'`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1728     TYPIFY `e'''` EXISTS_TAC;
1729     ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1730     REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1731     REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1732     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`];
1733     INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`3`;`4`];
1734     ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 4 = 7 /\ 3 + 3  = 6 /\ 3 <= 5 /\ 0 < 3 /\ 3 < 4 /\ 4 < 5`];
1735     DISCH_THEN (SUBST1_TAC o GSYM) THEN ASM_REWRITE_TAC[arith `x <= x`];
1736     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`];
1737     ASM_REWRITE_TAC[arith `x <= x`];
1738     INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`2`;`3`];
1739     NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[LET_THM];
1740     ASM_REWRITE_TAC[];
1741     ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN ASM_REWRITE_TAC[];
1742     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);
1743       BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
1744     BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1745   (DISCH_TAC);
1746   COMMENT "azim 0 additive";
1747   FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
1748   SUBCONJ_TAC;
1749     INTRO_TAC Cuxvzoz.epsilon_triple [`e'`;`e1'`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1750     TYPIFY `e''''` EXISTS_TAC;
1751     ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1752     REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1753     REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1754     MATCH_MP_TAC Fan.sum3_azim_fan;
1755     ASM_REWRITE_TAC[];
1756     BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);
1757   REPEAT WEAKER_STRIP_TAC;
1758   COMMENT "azim 1 additive";
1759   SUBCONJ_TAC;
1760     INTRO_TAC Cuxvzoz.epsilon_pair [`e''`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1761     TYPIFY `e'''` EXISTS_TAC;
1762     ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1763     REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1764     REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1765     MATCH_MP_TAC Fan.sum3_azim_fan;
1766     ASM_REWRITE_TAC[];
1767     CONJ_TAC;
1768       BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);
1769     ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
1770     ASM_REWRITE_TAC[];
1771     BY(CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
1772   REPEAT WEAKER_STRIP_TAC;
1773   COMMENT "pi bounds";
1774   CONJ_TAC;
1775     TYPIFY `e'` EXISTS_TAC;
1776     CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
1777     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;
1778       ASM_REWRITE_TAC[];
1779       MATCH_MP_TAC (arith `&0 <= b ==> (&0 < a /\ a < pi - b ==> &0 < a /\ a < pi)`);
1780       BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
1781     FIRST_X_ASSUM MATCH_MP_TAC;
1782     BY(ASM_REWRITE_TAC[]);
1783   MATCH_MP_TAC Oxl_def.periodic_numseg;
1784   TYPIFY `5` EXISTS_TAC;
1785   REWRITE_TAC[arith `~(5 = 0)`];
1786   CONJ_TAC;
1787     FIRST_X_ASSUM_ST `periodic` MP_TAC;
1788     REWRITE_TAC[Oxl_def.periodic];
1789     REWRITE_TAC[arith `(i+5)+j = (i+j)+5`];
1790     BY(DISCH_THEN (unlist REWRITE_TAC));
1791   REWRITE_TAC[IN_NUMSEG;arith `(0 <= i /\ i <= 5-1) <=> (i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4)`];
1792   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC;
1793           EXISTS_TAC `&1` THEN REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 4) < pi` MP_TAC);
1794           BY(MESON_TAC[arith `&0 < &1`;arith `x < pi ==> ~(x=pi)`]);
1795         REPEAT (FIRST_X_ASSUM_ST `+` kill);
1796         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);
1797         BY(MESON_TAC[arith `&0 < &1`;arith `x < pi ==> ~(x=pi)`]);
1798       BY(ASM_REWRITE_TAC[] THEN EXISTS_TAC `&1` THEN MESON_TAC[arith `&0 < &1`;arith `x <= x`]);
1799     INTRO_TAC Cuxvzoz.epsilon_triple [`e1''`;`e1'`;`e1`] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
1800     TYPIFY `e'''` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
1801     REPLICATE_TAC 3(FIRST_X_ASSUM (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC);
1802     REPEAT (FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1803     ASM_REWRITE_TAC[];
1804     FIRST_X_ASSUM_ST `a = pi` (SUBST1_TAC o GSYM);
1805     ASM_REWRITE_TAC[];
1806     BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1807   TYPIFY `e1'` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1808   REPEAT (FIRST_X_ASSUM_ST `4` (C INTRO_TAC [`t`]));
1809   ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1810   BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1811   ]);;
1812   (* }}} *)
1813 *)
1814
1815 let azim5_reduction = prove_by_refinement(
1816  `!s f v e.
1817      is_scs_v39 s /\
1818      scs_k_v39 s = 5 /\
1819      BBs_v39 s v /\
1820      scs_generic v /\
1821      deformation f (IMAGE v (:num)) (--e,e) /\
1822      (!w t. ~(w = v 4) /\ ~(w = v 0) ==> f w t = w) /\
1823      azim (vec 0) (v 0) (v 1) (v 4) < pi /\
1824      azim (vec 0) (v 1) (v 2) (v 0) < pi /\
1825      &0 < azim (vec 0) (v 0) (v 1) (v 3) /\
1826      (?e1. &0 < e1 /\
1827            (!t. abs t < e1
1828                 ==> azim (vec 0) (v 3) (f (v 0) t) (v 1) <=
1829                     azim (vec 0) (v 3) (v 0) (v 1))) /\
1830      (?e1. &0 < e1 /\
1831         (!t. abs t < e1
1832           ==> dist (v 3,f (v 4) t) = dist (v 3,v 4) /\
1833               dist (f (v 0) t,f (v 4) t) = dist (v 0,v 4) /\
1834               norm (f (v 4) t) = norm (v 4) /\
1835               dist (f (v 0) t,v 3) = dist (v 0,v 3) /\
1836               dist (f (v 0) t,v 1) = dist (v 0,v 1) - abs t /\
1837               norm (f (v 0) t) = norm (v 0) /\
1838             (coplanar {vec 0, v 3, v 4, v 0}
1839                                  ==> coplanar {vec 0, v 3, f (v 4) t, f (v 0) t})))
1840      ==> azim (vec 0) (v 3) (v 4) (v 2) =
1841          azim (vec 0) (v 3) (v 4) (v 0) +
1842          azim (vec 0) (v 3) (v 0) (v 1) +
1843          azim (vec 0) (v 3) (v 1) (v 2) /\
1844          azim (vec 0) (v 0) (v 1) (v 4) =
1845          azim (vec 0) (v 0) (v 1) (v 3) + azim (vec 0) (v 0) (v 3) (v 4) /\
1846          azim (vec 0) (v 1) (v 2) (v 0) =
1847          azim (vec 0) (v 1) (v 2) (v 3) + azim (vec 0) (v 1) (v 3) (v 0) /\
1848          (?e1. &0 < e1 /\
1849                (!t. abs t < e1
1850                     ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) =
1851                         azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) +
1852                         azim (vec 0) (v 3) (f (v 0) t) (v 1) +
1853                         azim (vec 0) (v 3) (v 1) (v 2) /\
1854                         azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) =
1855                         azim (vec 0) (f (v 0) t) (v 1) (v 3) +
1856                         azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) /\
1857                         azim (vec 0) (v 1) (v 2) (f (v 0) t) =
1858                         azim (vec 0) (v 1) (v 2) (v 3) +
1859                         azim (vec 0) (v 1) (v 3) (f (v 0) t) /\
1860                         &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\
1861                         azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi)) /\
1862          (!i. ?e0. &0 < e0 /\
1863                    (azim (vec 0) (v i) (v (i + 1)) (v (i + 4)) = pi
1864                     ==> (!t. abs t < e0
1865                              ==> azim (vec 0) (f (v i) t) (f (v (i + 1)) t)
1866                                  (f (v (i + 4)) t) <=
1867                                  pi))) /\
1868          (?e1. &0 < e1 /\
1869            (!t. abs t < e1
1870                 ==> azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) =
1871                     azim (vec 0) (v 3) (v 4) (v 0) /\
1872                     azim (vec 0) (f (v 4) t) (f (v 0) t) (v 3) =
1873                     azim (vec 0) (v 4) (v 0) (v 3) /\
1874                     azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) =
1875                     azim (vec 0) (v 0) (v 3) (v 4)))`,
1876   (* {{{ proof *)
1877   [
1878   REPEAT WEAKER_STRIP_TAC;
1879   ASSUME_TAC (arith `~(0 = 5)`);
1880   TYPIFY `!i. i MOD 5 < 5` (C SUBGOAL_THEN ASSUME_TAC);
1881     BY((FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[DIVISION]);
1882   TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
1883     BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
1884   TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
1885     GEN_TAC;
1886     MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
1887     BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
1888   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);
1889     FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
1890     BY(REWRITE_TAC[Ocbicby.MOD_5_EXPLICIT;arith `8 = 1*5 + 3`;arith `9 = 1*5 + 4`;MOD_MULT_ADD]);
1891   INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
1892   ASM_REWRITE_TAC[];
1893   DISCH_TAC;
1894   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);
1895     CONJ2_TAC;
1896       FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[LET_THM;Appendix.BBs_v39];
1897       BY(MESON_TAC[arith `~(5 <= 3)`]);
1898     BY(FIRST_X_ASSUM_ST `scs_generic` MP_TAC THEN MESON_TAC[Appendix.scs_generic]);
1899   FIRST_X_ASSUM MP_TAC THEN BURY_MP_TAC;
1900   COMMENT "first addition";
1901   SUBCONJ_TAC;
1902     INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`3`;`4`];
1903     ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 4 = 7 /\ 3 + 3  = 6 /\ 3 <= 5 /\ 0 < 3 /\ 3 < 4 /\ 4 < 5`];
1904     DISCH_THEN SUBST1_TAC;
1905     INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`2`;`3`];
1906     ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 3 = 6 /\ 3 + 2  = 5 /\ 3 <= 5 /\ 0 < 2 /\ 2 < 3 /\ 3 < 5`];
1907     DISCH_THEN SUBST1_TAC;
1908     BY(REAL_ARITH_TAC);
1909   DISCH_TAC;
1910   COMMENT "second addition";
1911   SUBCONJ_TAC;
1912     INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
1913     NUM_REDUCE_TAC;
1914     BY(ASM_REWRITE_TAC[LET_THM]);
1915   COMMENT "third addition";
1916   INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
1917   NUM_REDUCE_TAC;
1918   ASM_REWRITE_TAC[LET_THM];
1919   DISCH_TAC;
1920   DISCH_TAC;
1921   SUBCONJ_TAC;
1922     INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`1`;`2`;`4`];
1923     NUM_REDUCE_TAC;
1924     BY(ASM_REWRITE_TAC[LET_THM]);
1925   DISCH_TAC;
1926   TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i = j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
1927     BY(ASM_MESON_TAC[]);
1928   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);
1929     GEN_TAC;
1930     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);
1931   COMMENT "colinearity";
1932   TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0,v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
1933     REPEAT GEN_TAC THEN DISCH_TAC;
1934     MATCH_MP_TAC Zlzthic.PROPERTIES_GENERIC_LOCAL_FAN_ALT;
1935     GEXISTL_TAC [`IMAGE v (:num)`;`IMAGE (\i. {v i, v (SUC i)}) (:num)`;`IMAGE (\i. (v i, v (SUC i))) (:num)`];
1936     ASM_REWRITE_TAC[IN_IMAGE;IN_UNIV];
1937     CONJ_TAC;
1938       MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
1939       BY(ASM_REWRITE_TAC[]);
1940     BY(MESON_TAC[]);
1941   COMMENT "deform collinear";
1942   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);
1943     REPEAT WEAKER_STRIP_TAC;
1944     INTRO_TAC (GEN_ALL Local_lemmas1.CONTINUOUS_PRESERVE_COLLINEAR) [`&0`;`(vec 0):real^3`;`f (v i)`;`f (v j)`];
1945     ANTS_TAC;
1946       FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation;arith `abs(&0 - x) = abs x`];
1947       REWRITE_TAC[IN_IMAGE;IN_UNIV];
1948       BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
1949     BY(REWRITE_TAC[arith `abs(&0 - r') = abs r'`]);
1950   TYPIFY `!i. azim (vec 0) (v i) (v (i+1)) (v(i+4)) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
1951     REWRITE_TAC[arith `i+1 = SUC i`;arith `4 = 5 - 1`];
1952     GEN_TAC;
1953     MATCH_MP_TAC (REWRITE_RULE[LET_THM] Terminal.convex_local_fan_azim_le_pi);
1954     ASM_REWRITE_TAC[arith `3 <= 5`];
1955     FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM];
1956     BY(DISCH_THEN (unlist REWRITE_TAC));
1957   COMMENT "merge e";
1958   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);
1959     REPEAT WEAKER_STRIP_TAC;
1960     INTRO_TAC Cuxvzoz.epsilon_quad [`e1''`;`e1'''`;`e1''''`;`e1'''''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1961     TYPIFY `e''''` EXISTS_TAC;
1962     ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC THEN REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[];
1963       BY(ASM_MESON_TAC[]);
1964     BY(ASM_MESON_TAC[]);
1965   REWRITE_TAC[GSYM CONJ_ASSOC];
1966   COMMENT "azim bounds";
1967   TYPIFY `azim (vec 0) (v 0) (v 1) (v 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
1968     FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 4) < pi` MP_TAC;
1969     ASM_REWRITE_TAC[];
1970     MATCH_MP_TAC (arith `&0 <= y ==> (x + y < pi ==> x < pi)`);
1971     BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
1972   TYPIFY `~coplanar {vec 0,v 0,v 1,v 3}` (C SUBGOAL_THEN ASSUME_TAC);
1973     REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
1974     BY(REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 3)` MP_TAC) THEN REAL_ARITH_TAC);
1975   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);
1976     REWRITE_TAC[Zlzthic.azim_pos_iff_nz];
1977     FIRST_X_ASSUM_ST `coplanar` MP_TAC;
1978     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}`]);
1979   INTRO_TAC Cuxvzoz.WNWSHJT_ALT [`v 3`;`v 0`;`v 1`;`f`;`-- e`;`e`;`pi - azim (vec 0) (v 0) (v 3) (v 4)`];
1980   ANTS_TAC;
1981     ASM_REWRITE_TAC[arith `a < pi - b <=> a + b < pi`];
1982     CONJ_TAC;
1983       MATCH_MP_TAC Zlzthic.deformation_subset;
1984       TYPIFY `IMAGE v (:num)` EXISTS_TAC;
1985       ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_UNIV];
1986       BY(MESON_TAC[FUN_IN_IMAGE;IN_UNIV]);
1987     REWRITE_TAC[CONJ_ASSOC];
1988     CONJ_TAC;
1989       FIRST_X_ASSUM_ST `coplanar` MP_TAC;
1990       BY(MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan;SET_RULE `{a,b,c} = {a,c,b}`]);
1991     BY(REPEAT (FIRST_X_ASSUM_ST `x < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1992   REPEAT WEAKER_STRIP_TAC;
1993   INTRO_TAC Cuxvzoz.WNWSHJT_ALT [`v 0`;`v 1`;`v 3`;`f`;`-- e`;`e`;`pi - azim (vec 0) (v 1) (v 2) (v 3)`];
1994   ANTS_TAC;
1995     ASM_REWRITE_TAC[arith `a < pi - b <=> a + b < pi`];
1996     CONJ_TAC;
1997       MATCH_MP_TAC Zlzthic.deformation_subset;
1998       TYPIFY `IMAGE v (:num)` EXISTS_TAC;
1999       ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_UNIV];
2000       BY(MESON_TAC[FUN_IN_IMAGE;IN_UNIV]);
2001     REWRITE_TAC[CONJ_ASSOC];
2002     CONJ_TAC;
2003       FIRST_X_ASSUM_ST `coplanar` MP_TAC;
2004       BY(MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan;SET_RULE `{a,b,c} = {a,c,b}`]);
2005     BY(REPEAT (FIRST_X_ASSUM_ST `x < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
2006   REPEAT WEAKER_STRIP_TAC;
2007   COMMENT "034 triangle";
2008   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);
2009     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];
2010     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];
2011     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];
2012     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];
2013     INTRO_TAC Cuxvzoz.epsilon_quad [`e1''`;`e1'''`;`e1''''`;`e1'''''`] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2014     TYPIFY `e''''` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2015     BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);
2016   FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
2017   TYPIFY `!i. f (v i) (&0) = v i` (C SUBGOAL_THEN ASSUME_TAC);
2018     FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
2019     REPEAT WEAKER_STRIP_TAC;
2020     BY(FIRST_X_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC FUN_IN_IMAGE THEN REWRITE_TAC[IN_UNIV]);
2021   REWRITE_TAC[CONJ_ASSOC] THEN SUBCONJ2_TAC;
2022     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;
2023       FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
2024       INTRO_TAC Cuxvzoz.epsilon_triple [`e1'`;`e3`;`e2`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2025       TYPIFY `e'''` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2026       REPLICATE_TAC 3 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2027       REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2028       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);
2029         FIRST_X_ASSUM MP_TAC THEN (FIRST_X_ASSUM_ST `x <= pi` (C INTRO_TAC [`4`]));
2030         NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[];
2031         BY(MESON_TAC[Xivphks.FSQKWKK]);
2032       FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
2033       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))));
2034       REPLICATE_TAC 6 (POP_ASSUM GMATCH_SIMP_TAC);
2035       ASM_REWRITE_TAC[];
2036       ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN ASM_REWRITE_TAC[];
2037       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);
2038         BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2039       ASM_REWRITE_TAC[DIST_SYM];
2040       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[]);
2041     PROOF_BY_CONTR_TAC;
2042     FIRST_X_ASSUM kill;
2043     FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[];
2044     COMMENT "second half of assumption. All angles 034 <=pi";
2045     TYPIFY `coplanar {vec 0, v 3, v 4, v 0}` ASM_CASES_TAC;
2046       TYPIFY `e1'` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2047       FIRST_X_ASSUM_ST `coplanar` (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2048       FIRST_X_ASSUM MP_TAC;
2049       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);
2050         BY(SET_TAC[]);
2051       REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
2052       BY(MP_TAC PI_POS THEN REAL_ARITH_TAC);
2053     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;
2054     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);
2055       REWRITE_TAC[arith `&0 < x <=> &0 <= x /\ ~(x = &0) `;arith `x < pi <=> x <= pi /\ ~(x = pi)`];
2056       REWRITE_TAC[Counting_spheres.AZIM_NN];
2057       ASM_REWRITE_TAC[];
2058       FIRST_X_ASSUM_ST `a <= pi` (C INTRO_TAC [`4`]) THEN NUM_REDUCE_TAC;
2059       BY(ASM_REWRITE_TAC[]);
2060     TYPIFY `&0 < e` (C SUBGOAL_THEN ASSUME_TAC);
2061       FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation;IN_REAL_INTERVAL];
2062       BY(MESON_TAC[]);
2063     INTRO_TAC Cuxvzoz.epsilon_pair [`e3`;`e`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2064     INTRO_TAC Zlzthic.WNWSHJT [`v 3`;`v 4`;`v 0`;`f`;`-- e'''`;`e'''`] THEN ASM_REWRITE_TAC[];
2065     ANTS_TAC;
2066       TYPIFY_GOAL_THEN `~collinear {vec 0, v 4, v 0} /\ ~collinear {vec 0, v 4, v 3}` (unlist REWRITE_TAC);
2067         BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2068       MATCH_MP_TAC Cuxvzoz.deformation_restrict;
2069       TYPIFY `e` EXISTS_TAC THEN ASM_REWRITE_TAC[];
2070       MATCH_MP_TAC Zlzthic.deformation_subset;
2071       TYPIFY `(IMAGE v (:num))` EXISTS_TAC;
2072       ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
2073       BY(GEN_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC FUN_IN_IMAGE THEN REWRITE_TAC[IN_UNIV]);
2074     BY(MESON_TAC[arith `x < pi ==> x <= pi`]);
2075   (REPEAT WEAKER_STRIP_TAC THEN REWRITE_TAC[GSYM CONJ_ASSOC]);
2076   COMMENT "azim additivity";
2077   SUBCONJ_TAC;
2078     INTRO_TAC Cuxvzoz.epsilon_triple [`e1`;`e1''`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2079     TYPIFY `e'''` EXISTS_TAC;
2080     ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2081     REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2082     REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2083     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`];
2084     INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`3`;`4`];
2085     ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 4 = 7 /\ 3 + 3  = 6 /\ 3 <= 5 /\ 0 < 3 /\ 3 < 4 /\ 4 < 5`];
2086     DISCH_THEN (SUBST1_TAC o GSYM) THEN ASM_REWRITE_TAC[arith `x <= x`];
2087     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`];
2088     ASM_REWRITE_TAC[arith `x <= x`];
2089     INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`2`;`3`];
2090     NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[LET_THM];
2091     ASM_REWRITE_TAC[];
2092     ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN ASM_REWRITE_TAC[];
2093     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);
2094       BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2095     BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2096   COMMENT "azim 0 additive";
2097   REPEAT WEAKER_STRIP_TAC;
2098   SUBCONJ_TAC;
2099     INTRO_TAC Cuxvzoz.epsilon_triple [`e'`;`e1''`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2100     TYPIFY `e''''` EXISTS_TAC;
2101     ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2102     REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2103     REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2104     MATCH_MP_TAC Fan.sum3_azim_fan;
2105     ASM_REWRITE_TAC[];
2106     BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);
2107   REPEAT WEAKER_STRIP_TAC;
2108   COMMENT "azim 1 additive";
2109   SUBCONJ_TAC;
2110     INTRO_TAC Cuxvzoz.epsilon_pair [`e''`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2111     TYPIFY `e'''` EXISTS_TAC;
2112     ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2113     REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2114     REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2115     MATCH_MP_TAC Fan.sum3_azim_fan;
2116     ASM_REWRITE_TAC[];
2117     CONJ_TAC;
2118       BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);
2119     ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
2120     ASM_REWRITE_TAC[];
2121     BY(CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2122   REPEAT WEAKER_STRIP_TAC;
2123   COMMENT "pi bounds";
2124   CONJ_TAC;
2125     TYPIFY `e'` EXISTS_TAC;
2126     CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2127     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;
2128       ASM_REWRITE_TAC[];
2129       MATCH_MP_TAC (arith `&0 <= b ==> (&0 < a /\ a < pi - b ==> &0 < a /\ a < pi)`);
2130       BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
2131     FIRST_X_ASSUM MATCH_MP_TAC;
2132     BY(ASM_REWRITE_TAC[]);
2133   MATCH_MP_TAC Oxl_def.periodic_numseg;
2134   TYPIFY `5` EXISTS_TAC;
2135   REWRITE_TAC[arith `~(5 = 0)`];
2136   CONJ_TAC;
2137     FIRST_X_ASSUM_ST `periodic` MP_TAC;
2138     REWRITE_TAC[Oxl_def.periodic];
2139     REWRITE_TAC[arith `(i+5)+j = (i+j)+5`];
2140     BY(DISCH_THEN (unlist REWRITE_TAC));
2141   REWRITE_TAC[IN_NUMSEG;arith `(0 <= i /\ i <= 5-1) <=> (i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4)`];
2142   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC;
2143           EXISTS_TAC `&1` THEN REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 4) < pi` MP_TAC);
2144           BY(MESON_TAC[arith `&0 < &1`;arith `x < pi ==> ~(x=pi)`]);
2145         REPEAT (FIRST_X_ASSUM_ST `+` kill);
2146         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);
2147         BY(MESON_TAC[arith `&0 < &1`;arith `x < pi ==> ~(x=pi)`]);
2148       BY(ASM_REWRITE_TAC[] THEN EXISTS_TAC `&1` THEN MESON_TAC[arith `&0 < &1`;arith `x <= x`]);
2149     INTRO_TAC Cuxvzoz.epsilon_triple [`e1'''`;`e1''`;`e1`] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2150     TYPIFY `e'''` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2151     REPLICATE_TAC 3(FIRST_X_ASSUM (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC);
2152     REPEAT (FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2153     ASM_REWRITE_TAC[];
2154     FIRST_X_ASSUM_ST `a = pi` (SUBST1_TAC o GSYM);
2155     ASM_REWRITE_TAC[];
2156     BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
2157   TYPIFY `e1''` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2158   FIRST_X_ASSUM_ST `azim a b c d = azim a' b' c' d'` (C INTRO_TAC [`t`]);
2159   BY(ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[arith `x <= x`])
2160   ]);;
2161   (* }}} *)
2162
2163 let L13_LEMMA = prove_by_refinement(
2164   `main_nonlinear_terminal_v11
2165  ==>
2166  (!V E FF s v. IMAGE (\i. v i,v (SUC i)) (:num) = FF
2167  /\ is_scs_v39 s
2168  /\ scs_k_v39 s = 5
2169  /\ scs_basic_v39 s
2170  /\ scs_generic v
2171  /\ BBs_v39 s v
2172  /\ IMAGE v (:num) = V
2173  /\ IMAGE (\i. {v i, v (SUC i)}) (:num) = E
2174  /\ ~coplanar {vec 0, v 1, v 2, v 0}
2175  ==> &0 < azim (vec 0) (v 0) (v 1) (v 3) )`,
2176   (* {{{ proof *)
2177   [
2178   REPEAT WEAKER_STRIP_TAC;
2179   REWRITE_TAC[arith `&0 < a <=> ~(a = &0) /\ (&0 <= a)`];
2180   REWRITE_TAC[Counting_spheres.AZIM_NN];
2181   DISCH_TAC;
2182   FIRST_X_ASSUM_ST `coplanar {vec 0,v 1 ,v 2,v 0}` MP_TAC;
2183   REWRITE_TAC[];
2184   INTRO_TAC EGHNAVX_SCS [`s`;`5`;`v`;`0`];
2185   ASM_REWRITE_TAC[LET_THM];
2186   NUM_REDUCE_TAC;
2187   REPEAT WEAKER_STRIP_TAC;
2188   FIRST_X_ASSUM kill;
2189   FIRST_X_ASSUM (C INTRO_TAC [`3`;`2`]);
2190   NUM_REDUCE_TAC;
2191   ASM_REWRITE_TAC[];
2192   REPEAT WEAKER_STRIP_TAC;
2193   REWRITE_TAC[coplanar];
2194   GEXISTL_TAC [`(vec 0):real^3`;`v 0`;`v 1`];
2195   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;
2196     BY(SET_TAC[]);
2197   REWRITE_TAC[HULL_SUBSET];
2198   INTRO_TAC AFF_GT_SUBSET_AFFINE_HULL [`{vec 0,v 0}`;`{v 1}`];
2199   TYPIFY `{vec 0, v 0} UNION {v 1} = {vec 0, v 0, v 1}` (C SUBGOAL_THEN SUBST1_TAC);
2200     BY(SET_TAC[]);
2201   BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[])
2202   ]);;
2203   (* }}} *)
2204
2205 let IUNBUIG = prove_by_refinement(
2206   `main_nonlinear_terminal_v11 ==>
2207   (!s FF v.
2208   IMAGE (\i. (v i,v (SUC i))) (:num) = FF /\
2209   is_scs_v39 s /\
2210   scs_k_v39 s = 5 /\
2211   MMs_v39 s v /\
2212   scs_basic_v39 s /\
2213   scs_generic v /\
2214   (!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) /\
2215   scs_a_v39 s 0 1 = &2 /\
2216   scs_b_v39 s 0 1 <= cstab /\
2217      interior_angle1 (vec 0) FF (v 0) < pi /\      interior_angle1 (vec 0) FF (v 1) < pi /\
2218   (!i. ~(i MOD 5 = 0)  ==> dist(v i,v (i+1)) = &2) /\
2219   xrr (norm (v 0)) (norm (v 3)) (dist(v 0,v 3)) <= #15.53 /\
2220   xrr (norm (v 1)) (norm (v 3)) (dist(v 1,v 3)) <= #15.53 ==>
2221   dist(v 0,v 1) = &2)`,
2222   (* {{{ proof *)
2223   [
2224   REPEAT WEAKER_STRIP_TAC;
2225   TYPIFY `BBprime2_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
2226     BY(ASM_MESON_TAC[Appendix.scs_basic;Ayqjtmd.unadorned_MMs]);
2227   TYPIFY `BBprime_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
2228     BY(ASM_MESON_TAC[Appendix.BBprime2_v39]);
2229   TYPIFY `BBs_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
2230     BY(ASM_MESON_TAC[Appendix.BBprime_v39]);
2231   INTRO_TAC Appendix.BBs_v39 [`s`;`v`];
2232   ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;Terminal.IMAGE_SUBSET_IN;IN_UNIV;arith `~(5 <= 3)`];
2233   REPEAT WEAKER_STRIP_TAC;
2234   TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
2235   TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
2236   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
2237     MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
2238     BY(ASM_REWRITE_TAC[]);
2239   TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
2240     REPEAT WEAKER_STRIP_TAC;
2241     EXPAND_TAC "V";
2242     REWRITE_TAC[IN_IMAGE;IN_UNIV];
2243     BY(MESON_TAC[]);
2244   INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
2245   ASM_REWRITE_TAC[];
2246   DISCH_TAC;
2247   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);
2248     GEN_TAC;
2249     EXPAND_TAC "FF";
2250     GMATCH_SIMP_TAC (REWRITE_RULE[LET_THM] (GSYM Ocbicby.INTERIOR_ANGLE1_AZIM));
2251     TYPIFY `s` EXISTS_TAC;
2252     BY(ASM_REWRITE_TAC[IN;arith `5 - 1 = 4`;arith `3 < 5`;arith `SUC i = i+1`]);
2253   INTRO_TAC Ocbicby.LOCAL_FAN_AZIM_POS [`s`;`v`];
2254   ASM_REWRITE_TAC[LET_THM;IN;arith `5-1 = 4`;arith `SUC i = i+1`];
2255   DISCH_TAC;
2256   TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
2257     GEN_TAC;
2258     MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
2259     BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
2260   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);
2261     FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
2262     BY(REWRITE_TAC[Ocbicby.MOD_5_EXPLICIT;arith `8 = 1*5 + 3`;arith `9 = 1*5 + 4`;MOD_MULT_ADD]);
2263   TYPIFY `~coplanar {vec 0, v 0,v 1,v 4} /\ ~coplanar {vec 0,v 1,v 2,v 0}` (C SUBGOAL_THEN ASSUME_TAC);
2264     ASM_REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
2265     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`]);
2266   TYPIFY `generic V E` (C SUBGOAL_THEN ASSUME_TAC);
2267     BY(FIRST_X_ASSUM_ST `scs_generic` MP_TAC THEN ASM_REWRITE_TAC[Appendix.scs_generic]);
2268   INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
2269   NUM_REDUCE_TAC;
2270   ASM_REWRITE_TAC[LET_THM];
2271   DISCH_TAC;
2272   COMMENT "collinearity";
2273   TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0,v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
2274     REPEAT GEN_TAC THEN DISCH_TAC;
2275     MATCH_MP_TAC Zlzthic.PROPERTIES_GENERIC_LOCAL_FAN_ALT;
2276     GEXISTL_TAC [`IMAGE v (:num)`;`IMAGE (\i. {v i, v (SUC i)}) (:num)`;`IMAGE (\i. (v i, v (SUC i))) (:num)`];
2277     ASM_REWRITE_TAC[IN_IMAGE;IN_UNIV];
2278     BY(MESON_TAC[]);
2279   TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i = j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
2280     BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
2281   COMMENT "non coplanar 013 digression";
2282   INTRO_TAC (UNDISCH L13_LEMMA) [`V`;`E`;`FF`;`s`;`v`];
2283   ASM_REWRITE_TAC[];
2284   DISCH_TAC;
2285   REPEAT (FIRST_X_ASSUM_ST `interior_angle1 a b c < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC;
2286   REPEAT WEAKER_STRIP_TAC;
2287   TYPIFY `azim (vec 0) (v 0) (v 1) (v 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
2288     FIRST_X_ASSUM_ST `+` MP_TAC;
2289     MATCH_MP_TAC (arith `&0 <= a2 /\ a < pi   ==> (a = a1 + a2 ==> a1 < pi)`);
2290     REWRITE_TAC[Counting_spheres.AZIM_NN];
2291     BY(ASM_REWRITE_TAC[]);
2292   TYPIFY `~coplanar {vec 0,v 0, v 1,v 3}` (C SUBGOAL_THEN ASSUME_TAC);
2293     REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
2294     BY(REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2295   COMMENT "introduce deformation";
2296   INTRO_TAC deform_pent_exists [`V`;`(\t. -- abs t)`;`v 3`;`v 4`;`v 0`;`v 1`;`&1`];
2297   ASM_REWRITE_TAC[];
2298   REPEAT WEAKER_STRIP_TAC;
2299   FIRST_X_ASSUM MP_TAC;
2300   ANTS_TAC;
2301     REWRITE_TAC[arith `&0 < &1`;arith `--abs (&0) = &0`];
2302     CONJ_TAC;
2303       DISCH_TAC;
2304       INTRO_TAC coplanar_cross_reduction [`s`;`5`;`v`;`3`];
2305       NUM_REDUCE_TAC;
2306       BY(ASM_REWRITE_TAC[]);
2307     CONJ_TAC;
2308       FIRST_X_ASSUM MP_TAC;
2309       BY(MESON_TAC[SET_RULE `{a,b,c,d} = {a,d,b,c}`]);
2310     CONJ_TAC;
2311       BY(REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2312     CONJ_TAC;
2313       INTRO_TAC (GEN_ALL Local_lemmas.CONVEX_LOFA_IMP_INANGLE_LE_PI) [`E`;`V`;`FF`;`v 4`];
2314       ASM_REWRITE_TAC[];
2315       NUM_REDUCE_TAC;
2316       BY(ASM_REWRITE_TAC[]);
2317     CONJ_TAC;
2318       INTRO_TAC Trigonometry.JBDNJJB [`v 0`;`v 1`;`v 3`];
2319       TYPIFY `v 0 dot (v 1 cross v 3) = ((v 0 cross v 1) dot v 3)` (C SUBGOAL_THEN SUBST1_TAC);
2320         BY(VEC3_TAC);
2321       REWRITE_TAC[arith `x > &0 <=> &0 < x`];
2322       ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
2323       REWRITE_TAC[Trigonometry2.re_eqvl];
2324       REPEAT WEAKER_STRIP_TAC;
2325       ASM_REWRITE_TAC[];
2326       GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
2327       BY(ASM_REWRITE_TAC[Cuxvzoz.sin_azim_pos]);
2328     GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
2329     REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
2330     REPEAT WEAKER_STRIP_TAC;
2331     MATCH_MP_TAC REAL_CONTINUOUS_NEG;
2332     BY(REWRITE_TAC[Cuxvzoz.real_continuous_abs]);
2333   REPEAT WEAKER_STRIP_TAC;
2334   (COMMENT "reduction lemmas");
2335   PROOF_BY_CONTR_TAC;
2336   TYPIFY `&2 < dist(v 0,v 1)` (C SUBGOAL_THEN ASSUME_TAC);
2337     FIRST_X_ASSUM_ST `scs_a_v39` (C INTRO_TAC [`0`;`1`]);
2338     BY(ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
2339   FIRST_X_ASSUM_ST `~` MP_TAC THEN REWRITE_TAC[];
2340   TYPIFY `!i. f (v i) (&0) = v i` (C SUBGOAL_THEN ASSUME_TAC);
2341     FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
2342     BY(ASM_MESON_TAC[]);
2343   INTRO_TAC a5_assumption_reduction [`s`;`f`;`v`;`e'`];
2344   ASM_REWRITE_TAC[];
2345   ANTS_TAC;
2346     CONJ_TAC;
2347       REPEAT WEAKER_STRIP_TAC;
2348       FIRST_X_ASSUM_ST `scs_diag` (C INTRO_TAC [`i`;`j`]);
2349       BY(ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
2350     CONJ_TAC;
2351       TYPIFY `e'` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2352       FIRST_X_ASSUM (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[DIST_SYM];
2353       BY(MESON_TAC[]);
2354     INTRO_TAC Cuxvzoz.continuous_nbd_pos [`\ t. dist(f (v 0) t,v 1) - &2`;`&0`];
2355     ASM_REWRITE_TAC[arith `abs (t' - &0) = abs t'`;arith `&0 < a - b <=> b < a`];
2356     ANTS_TAC;
2357       FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
2358       REPEAT WEAKER_STRIP_TAC;
2359       FIRST_X_ASSUM_ST `atreal` (C INTRO_TAC [`v 0`;`&0`]);
2360       ASM_REWRITE_TAC[];
2361       DISCH_TAC;
2362       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]))));
2363     BY(MESON_TAC[arith `x < y ==> x <= y`]);
2364   DISCH_TAC;
2365   (COMMENT "b5 reduction");
2366   INTRO_TAC b5_assumption_reduction [`s`;`f`;`v`;`e'`];
2367   ASM_REWRITE_TAC[];
2368   ANTS_TAC;
2369     CONJ_TAC;
2370       BY(ASM_MESON_TAC[]);
2371     CONJ_TAC;
2372       TYPIFY `e'` EXISTS_TAC;
2373       FIRST_X_ASSUM_ST `norm` MP_TAC THEN ASM_REWRITE_TAC[DIST_SYM];
2374       BY(MESON_TAC[]);
2375     TYPIFY `e'` EXISTS_TAC;
2376     CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2377     FIRST_X_ASSUM_ST `norm` (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[DIST_SYM];
2378     DISCH_THEN (unlist REWRITE_TAC);
2379     BY(REAL_ARITH_TAC);
2380   DISCH_TAC;
2381   COMMENT "deform collinear";
2382   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);
2383     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);
2384   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);
2385     REPEAT WEAKER_STRIP_TAC;
2386     INTRO_TAC (GEN_ALL Local_lemmas1.CONTINUOUS_PRESERVE_COLLINEAR) [`&0`;`(vec 0):real^3`;`f (v i)`;`f (v j)`];
2387     REWRITE_TAC[arith `abs(&0 - r') = abs r'`] THEN DISCH_THEN MATCH_MP_TAC;
2388     ASM_REWRITE_TAC[];
2389     FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
2390     REPEAT WEAKER_STRIP_TAC;
2391     REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC;
2392       BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
2393     FIRST_X_ASSUM MATCH_MP_TAC;
2394     FIRST_X_ASSUM MATCH_MP_TAC;
2395     BY(ASM_MESON_TAC[]);
2396   TYPIFY `!i. azim (vec 0) (v i) (v (i+1)) (v(i+4)) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
2397     REWRITE_TAC[arith `i+1 = SUC i`;arith `4 = 5 - 1`];
2398     GEN_TAC;
2399     MATCH_MP_TAC (REWRITE_RULE[LET_THM] Terminal.convex_local_fan_azim_le_pi);
2400     ASM_REWRITE_TAC[arith `3 <= 5`];
2401     FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM];
2402     BY(ASM_REWRITE_TAC[]);
2403   COMMENT "coplanar";
2404   INTRO_TAC Zlzthic.NONPLANAR_OPEN [`(\ (t:real). (vec 0):real^3)`;`f (v 0)`;`\ (t:real). v 1`;`\ (t:real). v 3`;`&0`];
2405   ASM_REWRITE_TAC[CONTINUOUS_CONST];
2406   ANTS_TAC;
2407     FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation] THEN REPEAT WEAKER_STRIP_TAC;
2408     BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
2409   REWRITE_TAC[arith `abs (&0 - t') = abs t'`] THEN REPEAT WEAKER_STRIP_TAC;
2410   COMMENT "azim reduction";
2411   INTRO_TAC azim5_reduction [`s`;`f`;`v`;`e'`];
2412   ASM_REWRITE_TAC[];
2413   ANTS_TAC;
2414     CONJ_TAC;
2415       BY(REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `a < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[]);
2416     CONJ2_TAC;
2417       TYPIFY `e'` EXISTS_TAC;
2418       BY(ASM_REWRITE_TAC[arith `x - abs t = x + --abs t`]);
2419     INTRO_TAC Zlzthic.WNWSHJT [`v 1`;`v 3`;`v 0`;`f`;`-- e'`;`e'`];
2420     ASM_REWRITE_TAC[];
2421     ANTS_TAC;
2422       CONJ_TAC;
2423         MATCH_MP_TAC Zlzthic.deformation_subset;
2424         TYPIFY `V` EXISTS_TAC;
2425         ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
2426         BY(EXPAND_TAC "V" THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC FUN_IN_IMAGE THEN REWRITE_TAC[IN_UNIV]);
2427       TYPIFY_GOAL_THEN `~collinear {vec 0, v 3, v 0} /\ ~collinear {vec 0, v 3, v 1}` (unlist REWRITE_TAC);
2428         BY(CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2429       FIRST_X_ASSUM_ST `coplanar` kill;
2430       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];
2431       REWRITE_TAC[arith `&0 < a <=> &0 <= a /\ ~(a = &0)`];
2432       REWRITE_TAC[Counting_spheres.AZIM_NN];
2433       REWRITE_TAC[arith `a < pi <=> a <= pi /\ ~(a = pi)`;DE_MORGAN_THM];
2434       DISCH_THEN (unlist REWRITE_TAC);
2435       REPLICATE_TAC 2(MATCH_MP_TAC Xivphks.FSQKWKK);
2436       FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`0`]) THEN NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[];
2437       MATCH_MP_TAC (arith `&0 <= a2 ==> (a1 + a2 <= pi ==> a1 <= pi)`);
2438       BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
2439     (REPEAT WEAKER_STRIP_TAC);
2440     INTRO_TAC Cuxvzoz.epsilon_triple [`e`;`e''`;`e'`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2441     TYPIFY `e''''` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2442     REPLICATE_TAC 3 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2443     INTRO_TAC azim_dih_y [`(vec 0):real^3`;`v 3`;`f (v 0) t`;`v 1`];
2444     INTRO_TAC azim_dih_y [`(vec 0):real^3`;`v 3`;`(v 0)`;`v 1`];
2445     DISCH_THEN GMATCH_SIMP_TAC;
2446     CONJ_TAC;
2447       FIRST_X_ASSUM_ST `x < pi` (C INTRO_TAC [`&0`]) THEN ASM_REWRITE_TAC[arith `abs(&0) = &0`];
2448       SIMP_TAC[arith `x < pi ==> x <= pi`];
2449       DISCH_TAC;
2450       BY(CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2451     DISCH_THEN GMATCH_SIMP_TAC;
2452     CONJ_TAC;
2453       REWRITE_TAC[CONJ_ASSOC] THEN CONJ2_TAC;
2454         MATCH_MP_TAC (arith `x < pi ==> x <= pi`);
2455         BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
2456       CONJ_TAC;
2457         ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
2458         BY(FIRST_X_ASSUM_ST `coplanar` (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan]);
2459       BY(REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2460     FIRST_X_ASSUM_ST `norm` (C INTRO_TAC [`t`]);
2461     ASM_REWRITE_TAC[DIST_SYM;DIST_0];
2462     REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[];
2463     MATCH_MP_TAC Ocbicby.dih_y_mono;
2464     FIRST_X_ASSUM_ST `~coplanar s` (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[];
2465     FIRST_X_ASSUM_ST `~coplanar s` MP_TAC;
2466     REPEAT WEAKER_STRIP_TAC;
2467     REWRITE_TAC[arith `d + -- abs t <= d`];
2468     CONJ_TAC;
2469       REWRITE_TAC[NORM_POS_LT];
2470       POP_ASSUM (MP_TAC o (MATCH_MP Planarity.notcoplanar_disjoint));
2471       BY(MESON_TAC[]);
2472     CONJ_TAC;
2473       FIRST_X_ASSUM_ST `abs` (SUBST1_TAC o GSYM);
2474       REWRITE_TAC[GSYM DIST_NZ];
2475       POP_ASSUM (MP_TAC o (MATCH_MP Planarity.notcoplanar_disjoint));
2476       BY(MESON_TAC[]);
2477     CONJ_TAC;
2478       POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Oxlzlez.coplanar_delta_y;DIST_SYM;DIST_0];
2479       BY(MESON_TAC[Merge_ineq.delta_y_sym]);
2480     INTRO_TAC Terminal.DELTA_Y_POS_4POINTS [`(vec 0):real^3`;`v 3`;`v 0`;`v 1`];
2481     BY(REWRITE_TAC[DIST_0;DIST_SYM]);
2482   REPEAT WEAKER_STRIP_TAC;
2483   (COMMENT "end of azim reduction");
2484   COMMENT "deformation in BBs";
2485   INTRO_TAC Cuxvzoz.deformation_BBs_ALT [`s`;`5`;`f`;`v`;`e'`];
2486   NUM_REDUCE_TAC;
2487   ASM_REWRITE_TAC[];
2488   ANTS_TAC;
2489     MATCH_MP_TAC Terminal.periodic_mod_reduce;
2490     TYPIFY `5` EXISTS_TAC THEN REWRITE_TAC[arith `~(5 = 0)`];
2491     CONJ_TAC;
2492       FIRST_X_ASSUM_ST `periodic` MP_TAC THEN REWRITE_TAC[Oxl_def.periodic];
2493       BY(MESON_TAC[]);
2494     REWRITE_TAC[arith `i < 5 <=> i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4`];
2495     REPEAT WEAKER_STRIP_TAC THEN (FIRST_X_ASSUM_ST `norm` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2496     BY(FIRST_X_ASSUM_ST ` \/ ` MP_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
2497   REPEAT WEAKER_STRIP_TAC;
2498   COMMENT "back to root, next tau";
2499   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);
2500     REPEAT WEAKER_STRIP_TAC;
2501     MATCH_MP_TAC Cuxvzoz.MMs_minimize_tau_fun;
2502     TYPIFY `s` EXISTS_TAC;
2503     ASM_REWRITE_TAC[arith `3 < 5`];
2504     FIRST_X_ASSUM MATCH_MP_TAC;
2505     BY(FIRST_X_ASSUM (unlist REWRITE_TAC));
2506   POP_ASSUM MP_TAC;
2507   TYPIFY `{i | i < 5} = 0..4` (C SUBGOAL_THEN SUBST1_TAC);
2508     BY(REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC);
2509   REWRITE_TAC[SUM_NUMSEG4];
2510   NUM_REDUCE_TAC;
2511   DISCH_TAC;
2512   COMMENT "introduce nonlinear 684";
2513   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);
2514     BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
2515   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)`];
2516   ASM_REWRITE_TAC[];
2517   ANTS_TAC;
2518     ONCE_REWRITE_TAC[Ocbicby.xrr_sym];
2519     ASM_REWRITE_TAC[GSYM Sphere.cstab];
2520     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);
2521       REWRITE_TAC[GSYM Fnjlbxs.in_ball_annulus];
2522       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;
2523       FIRST_X_ASSUM_ST `ball_annulus` MP_TAC;
2524       REWRITE_TAC[SUBSET;IN_IMAGE;IN_UNIV];
2525       BY(MESON_TAC[]);
2526     REWRITE_TAC[ CONJ_ASSOC] THEN CONJ2_TAC;
2527       INTRO_TAC Oxlzlez.coplanar_delta_y [`(vec 0):real^3`;`v 3`;`v 0`;`v 1`];
2528       REWRITE_TAC[DIST_0;DIST_SYM] THEN DISCH_THEN (SUBST1_TAC o GSYM);
2529       BY(ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {a,c,d,b}`] THEN ASM_REWRITE_TAC[]);
2530     TYPIFY_GOAL_THEN `(&2 <= dist (v 0,v 1) /\ dist (v 0,v 1) <= cstab)` (unlist REWRITE_TAC);
2531       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;
2532       BY(REAL_ARITH_TAC);
2533     CONJ_TAC;
2534       REPEAT (FIRST_X_ASSUM_ST `scs_a_v39` (C INTRO_TAC [`1`;`3`]) );
2535       BY(ASM_REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
2536     REPEAT (FIRST_X_ASSUM_ST `scs_a_v39` (C INTRO_TAC [`0`;`3`]) );
2537     BY(ASM_REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
2538   REPEAT WEAKER_STRIP_TAC;
2539   PROOF_BY_CONTR_TAC;
2540   FIRST_X_ASSUM_ST `IN` MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;TAUT `~(a ==> b) <=> (a /\ ~b)`;arith `~(a < b) <=> b <= a`];
2541   TYPIFY `?e2. &0 < e2 /\ (!t. abs t < e2 ==> dist(v 0,v 1) + t IN real_interval(a,b))` (C SUBGOAL_THEN MP_TAC);
2542     INTRO_TAC Zlzthic.real_interval_contains_0_ball [`a-dist(v 0,v 1)`;`b - dist(v 0,v 1)`;`&1`];
2543     REWRITE_TAC[arith `&0 < &1`;arith `a - d < &0 <=> a < d`;arith `&0 < b - d <=> d < b`];
2544     ANTS_TAC;
2545       FIRST_X_ASSUM_ST `dist s IN real_interval (a,b)` MP_TAC;
2546       BY(REWRITE_TAC[IN_REAL_INTERVAL]);
2547     REPEAT WEAKER_STRIP_TAC;
2548     TYPIFY `e'''` EXISTS_TAC;
2549     (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]);
2550     BY(REAL_ARITH_TAC);
2551   REPEAT WEAKER_STRIP_TAC;
2552   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;
2553     REPEAT WEAKER_STRIP_TAC;
2554     GEXISTL_TAC [`dist(v 0,v 1) + t`;`dist(v 0,v 1)`];
2555     ASM_REWRITE_TAC[];
2556     CONJ2_TAC;
2557       BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2558     FIRST_X_ASSUM MATCH_MP_TAC;
2559     BY(ASM_REWRITE_TAC[]);
2560   COMMENT "choose epsilon and t";
2561   INTRO_TAC epsilon_hex [`e`;`e'`;`e''`;`e1`;`e1'`;`e2`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2562   TYPIFY `?t. t < &0 /\ abs t < e6` (C SUBGOAL_THEN MP_TAC);
2563     TYPIFY `-- e6 / &2` EXISTS_TAC;
2564     BY(FIRST_X_ASSUM_ST `&0 < e6` MP_TAC THEN REAL_ARITH_TAC);
2565   REPEAT WEAKER_STRIP_TAC;
2566   REPLICATE_TAC 6 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2567   TYPIFY `t` EXISTS_TAC THEN ASM_REWRITE_TAC[];
2568   REPLICATE_TAC 8 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2569   FIRST_X_ASSUM_ST `rho_fun` MP_TAC THEN ASM_REWRITE_TAC[Appendix.rho_rho_fun];
2570   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`];
2571   MATCH_MP_TAC (arith `a - (pi+sol0) = a' /\ b - (pi+sol0) = b' ==> (a <= b ==> a' <= b')`);
2572   REWRITE_TAC[arith `(a + b+c) - (pi + sol0) = a + b + c - (pi + sol0)`];
2573   CONJ_TAC;
2574     GMATCH_SIMP_TAC (GSYM Cuxvzoz.tau3_azim);
2575     GMATCH_SIMP_TAC Cuxvzoz.tau3_taum_nonplanar;
2576     ASM_REWRITE_TAC[];
2577     REWRITE_TAC[DIST_SYM];
2578     CONJ2_TAC;
2579       BY(MESON_TAC[Terminal.taum_sym]);
2580     BY(REPEAT (FIRST_X_ASSUM_ST `a < pi` MP_TAC) THEN REAL_ARITH_TAC);
2581   FIRST_X_ASSUM_ST `norm a  = norm b` (SUBST1_TAC o GSYM);
2582   TYPIFY `dist(v 0,v 1) + t = dist(v 0,v 1) + -- abs t` (C SUBGOAL_THEN SUBST1_TAC);
2583     BY(FIRST_X_ASSUM_ST `t < &0` MP_TAC THEN REAL_ARITH_TAC);
2584   FIRST_X_ASSUM_ST `d = d' + -- abs t` (SUBST1_TAC o GSYM);
2585   GMATCH_SIMP_TAC (GSYM Cuxvzoz.tau3_azim);
2586   GMATCH_SIMP_TAC Cuxvzoz.tau3_taum_nonplanar;
2587   REWRITE_TAC[DIST_SYM];
2588   REWRITE_TAC[CONJ_ASSOC] THEN CONJ2_TAC;
2589     ASM_REWRITE_TAC[DIST_SYM];
2590     BY(MESON_TAC[Terminal.taum_sym]);
2591   ASM_REWRITE_TAC[];
2592   FIRST_X_ASSUM_ST `a < pi` MP_TAC;
2593   BY(REAL_ARITH_TAC)
2594   ]);;
2595   (* }}} *)
2596
2597 end;;