legacy/oldleg/collect_geom_spec.ml

   1 (* Nguyen Quang Truong *)\r
   2 needs "Multivariate/vectors.ml";; (* Eventually should load entire *)      \r
   3 needs "Examples/analysis.ml";; (* multivariate-complex theory. *)          \r
   4 needs "Examples/transc.ml";; (* Then it won't need these three. *)\r
   5 needs "convex_header.ml";; \r
   6 needs "definitions_kepler.ml";;\r
   7 let ups_x = new_definition ` ups_x x1 x2 x6 =\r
   8          --x1 * x1 - x2 * x2 - x6 * x6 +\r
   9          &2 * x1 * x6 +\r
  10          &2 * x1 * x2 +\r
  11          &2 * x2 * x6 `;;\r
  12 let rho = new_definition ` rho (x12 :real) x13 x14 x23 x24 x34 =\r
  13          --(x14 * x14 * x23 * x23) -\r
  14          x13 * x13 * x24 * x24 -\r
  15          x12 * x12 * x34 * x34 +\r
  16          &2 *\r
  17          (x12 * x14 * x23 * x34 +\r
  18           x12 * x13 * x24 * x34 +\r
  19           x13 * x14 * x23 * x24) `;;\r
  20 let chi = new_definition ` chi x12 x13 x14 x23 x24 x34 =\r
  21          x13 * x23 * x24 +\r
  22          x14 * x23 * x24 +\r
  23          x12 * x23 * x34 +\r
  24          x14 * x23 * x34 +\r
  25          x12 * x24 * x34 +\r
  26          x13 * x24 * x34 -\r
  27          &2 * x23 * x24 * x34 -\r
  28          x12 * x34 * x34 -\r
  29          x14 * x23 * x23 -\r
  30          x13 * x24 * x24 `;;\r
  31 let delta = new_definition ` delta x12 x13 x14 x23 x24 x34 =\r
  32    --(x12 * x13 * x23) -\r
  33          x12 * x14 * x24 -\r
  34          x13 * x14 * x34 -\r
  35          x23 * x24 * x34 +\r
  36          x12 * x34 * (--x12 + x13 + x14 + x23 + x24 - x34) + \r
  37          x13 * x24 * (x12 - x13 + x14 + x23 - x24 + x34 ) +\r
  38          x14 * x23 * ( x12 + x13 - x14 - x23 + x24 + x34 ) `;;\r
  39 \r
  40 let eta_v = new_definition ` eta_v v1 v2 (v3: real^N) =\r
  41         let e1 = dist (v2, v3) in\r
  42           let e2 = dist (v1, v3) in\r
  43           let e3 = dist (v2, v1) in\r
  44           e1 * e2 * e3 / sqrt ( ups_x (e1 pow 2 ) ( e2 pow 2) ( e3 pow 2 ) ) `;;\r
  45 \r
  46 let plane_norm = new_definition `\r
  47   plane_norm p <=>\r
  48          (?n v0. ~(n = vec 0) /\ p = {v | n dot (v - v0) = &0}) `;;\r
  49 \r
  50 let circumradius = new_definition ` circumradius s = (@r. ? x. x IN s /\\r
  51   r = dist( x , circumcenter s ) )`;;\r
  52 \r
  53 let delta_x12 = new_definition ` delta_x12 x12 x13 x14 x23 x24 x34 =\r
  54   -- x13 * x23 + -- x14 * x24 + x34 * ( -- x12 + x13 + x14 + x23 + x24 + -- x34 )\r
  55   + -- x12 * x34 + x13 * x24 + x14 * x23 `;;\r
  56 \r
  57 let delta_x13 = new_definition` delta_x13 x12 x13 x14 x23 x24 x34 =\r
  58   -- x12 * x23 + -- x14 * x34 + x12 * x34 + x24 * ( x12 + -- x13 + x14 + x23 + \r
  59   -- x24 + x34 ) + -- x13 * x24 + x14 * x23 `;;\r
  60 \r
  61 let delta_x14 = new_definition`delta_x14 x12 x13 x14 x23 x24 x34 =\r
  62          --x12 * x24 +\r
  63          --x13 * x34 +\r
  64          x12 * x34 +\r
  65          x13 * x24 +\r
  66          x23 * (x12 + x13 + --x14 + --x23 + x24 + x34) +\r
  67          --x14 * x23`;;\r
  68 \r
  69 let delta_x34 = new_definition` delta_x34 x12 x13 x14 x23 x24 x34 =\r
  70 -- &2 * x12 * x34 +\r
  71      --x13 * x14 +\r
  72      --x23 * x24 +\r
  73      x13 * x24 +\r
  74      x14 * x23 +\r
  75      --x12 * x12 +\r
  76      x12 * x14 +\r
  77      x12 * x24 +\r
  78      x12 * x13 +\r
  79      x12 * x23`;;\r
  80 \r
  81 let delta_x23 = new_definition ` delta_x23 x12 x13 x14 x23 x24 x34 =\r
  82          --x12 * x13 +\r
  83          --x24 * x34 +\r
  84          x12 * x34 +\r
  85          x13 * x24 +\r
  86          --x14 * x23 +\r
  87          x14 * (x12 + x13 - x14 - x23 + x24 + x34) `;;\r
  88 \r
  89 \r
  90 let max_real3 = new_definition ` max_real3 x y z = max_real (max_real x y ) z `;;\r
  91 let ups_x_pow2 = new_definition` ups_x_pow2 x y z = ups_x ( x*x ) ( y * y) ( z * z)`;;\r
  92 \r
  93 \r
  94 let condA = new_definition `condA (v1:real^3) v2 v3 v4 x12 x13 x14 x23 x24 x34 = \r
  95   ( ~ ( v1 = v2 ) /\ coplanar {v1,v2,v3,v4} /\\r
  96   ( dist ( v1, v2) pow 2 ) = x12 /\\r
  97   dist (v1,v3) pow 2 = x13 /\\r
  98   dist (v1,v4) pow 2 = x14 /\\r
  99   dist (v2,v3) pow 2 = x23 /\ dist (v2,v4) pow 2 = x24 )`;;\r
 100 (* def 26. p 22 *)\r
 101 let condC = new_definition ` condC M13 m12 m14 M24 m34 (m23:real) =\r
 102   ((! x. x IN {M13, m12, m14, M24, m34, m23 } ==> &0 <= x ) /\\r
 103   M13 <= m12 + m23 /\\r
 104   M13 <= m14 + m34 /\ \r
 105   M24 < m12 + m14 /\\r
 106   M24 < m23 + m34 /\ \r
 107   &0 <= delta (M13 pow 2) (m12 pow 2) (m14 pow 2) (M24 pow 2) (m34 pow 2 )\r
 108    (m23 pow 2 ) )`;;\r
 109 \r
 110 let condF = new_definition` condF m14 m24 m34 M23 M13 M12 =\r
 111          ((!x. x IN {m14, m24, m34, M23, M13, M12} ==> &0 < x) /\\r
 112          M12 < m14 + m24 /\\r
 113          M13 < m14 + m34 /\\r
 114          M23 < m24 + m34 /\\r
 115          &0 <\r
 116          delta (m14 pow 2) (m24 pow 2) (m34 pow 2) (M23 pow 2) (M13 pow 2)\r
 117          (M12 pow 2)) `;;\r
 118 \r
 119 let condS = new_definition ` condS m m34 M13 M23 <=>\r
 120      (!t. t IN {m, m34, M13, M23} ==> &0 < t) /\\r
 121      M13 < m + m34 /\\r
 122      M23 < m + m34 /\\r
 123      M13 pow 2 < M23 pow 2 + &4 * m * m /\\r
 124      M23 pow 2 < M13 pow 2 + &4 * m * m /\\r
 125      (!r. delta (&4 * m * m) (M13 pow 2) (M23 pow 2) r (M13 pow 2) (M23 pow 2) = &0\r
 126           ==> r < &4 * m34 * m34) `;;\r
 127 \r
 128 let cos_arc = new_definition` cos_arc (a:real) b c = \r
 129    ( a pow 2 + b pow 2 - c pow 2 )/ ( &2 * a * b ) `;;\r
 130 \r
 131 let muy_v = new_definition ` muy_v (x1: real^N ) (x2:real^N) (x3:real^N) (x4:real^N)\r
 132 (x5:real^N) x45 = \r
 133           (let x12 = dist (x1,x2) pow 2 in\r
 134           let x13 = dist (x1,x3) pow 2 in\r
 135           let x14 = dist (x1,x4) pow 2 in\r
 136           let x15 = dist (x1,x5) pow 2 in\r
 137           let x23 = dist (x2,x3) pow 2 in\r
 138           let x24 = dist (x2,x4) pow 2 in\r
 139           let x25 = dist (x2,x5) pow 2 in\r
 140           let x34 = dist (x3,x4) pow 2 in\r
 141           let x35 = dist (x3,x5) pow 2 in\r
 142           cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45) `;;\r
 143 (* dedinition of E. page 34 *)\r
 144 let sqrt_of_ge_root = new_definition `\r
 145 sqrt_of_ge_root y14 y24 y34 y12 y13 y23 y15 y25 y35 =\r
 146          (@r. ?le ge a.\r
 147                   le <= ge /\\r
 148                   r = sqrt ge /\\r
 149                   (!x. cayleyR (y12 pow 2) (y13 pow 2) (y14 pow 2)\r
 150                        (y15 pow 2)\r
 151                        (y23 pow 2)\r
 152                        (y24 pow 2)\r
 153                        (y25 pow 2)\r
 154                        (y34 pow 2)\r
 155                        (y35 pow 2)\r
 156                        x =\r
 157                        a * (x - le) * (x - ge))) `;;\r
 158 (* Lemma 2, page 6 *)\r
 159 let RHUFIIB =  ` !x12 x13 x14 x23 x24 x34.\r
 160          rho x12 x13 x14 x23 x24 x34 * ups_x x34 x24 x23 =\r
 161          chi x12 x13 x14 x23 x24 x34 pow 2 +\r
 162          &4 * delta x12 x13 x14 x23 x24 x34 * x34 * x24 * x23 `;;\r
 163 (* Lemma 3, *)\r
 164 let NUHSVLM =  ` !x1 x2 x3 x4 (x5 :real^3). \r
 165                  let x12 = dist (x1,x2) pow 2 in\r
 166          let x13 = dist (x1,x3) pow 2 in\r
 167          let x14 = dist (x1,x4) pow 2 in\r
 168          let x15 = dist (x1,x5) pow 2 in\r
 169          let x23 = dist (x2,x3) pow 2 in\r
 170          let x24 = dist (x2,x4) pow 2 in\r
 171          let x25 = dist (x2,x5) pow 2 in\r
 172          let x34 = dist (x3,x4) pow 2 in\r
 173          let x35 = dist (x3,x5) pow 2 in\r
 174          let x45 = dist (x4,x5) pow 2 in\r
 175          &0 <= ups_x x12 x13 x23 /\\r
 176          &0 <= delta x12 x13 x14 x23 x24 x34 /\\r
 177          cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 = &0 `;;\r
 178 (* lemma 4, page 7 *)\r
 179 let JVUNDLC =  ` ! a b (c:real ) s. s = ( a + b + c ) / &2 ==>\r
 180  &16 * s * (s - a) * (s - b) * (s - c) =\r
 181              ups_x (a pow 2) (b pow 2) (c pow 2)`;;\r
 182 (* lemma 5, page 12 *)\r
 183 let RCEABUJ =  ` ! a (b:real^3) x. line x /\ {a,b} SUBSET x /\ ~( a = b) \r
 184     ==> x = aff {a,b} `;;\r
 185 (* lem 6. p 12 *)\r
 186 let BXVMKNF =  ` ! u v:real ^3. ~( u=v) ==> plane_norm ( bis u v ) `;;\r
 187 (* la 7. p 12 *)\r
 188 let SMWTDMU =  ` !x y z p.\r
 189          plane p /\ ~collinear {x, y, z} /\ {x, y, z} SUBSET p\r
 190          ==> p = aff {x, y, z}`;;\r
 191 (* le 8. p 12 *)\r
 192 let SGFCDZO =  `! v1 v2 v3:real^3 t1 t2 (t3:real). \r
 193          t1 % v1 + t2 % v2 + t3 % v3 = vec 0 /\\r
 194          t1 + t2 + t3 = &0 /\\r
 195          ~(t1 = &0 /\ t2 = &0 /\ t3 = &0)\r
 196          ==> collinear {v1, v2, v3}`;;\r
 197 let lemma8 = SGFCDZO;;\r
 198 (* le 9. p 13 *)\r
 199 let FHFMKIY =  ` ! (v1: real^3) v2 v3 x12 x13 x23.\r
 200          x12 = dist (v1,v2) pow 2 /\\r
 201          x13 = dist (v1,v3) pow 2 /\\r
 202          x23 = dist (v2,v3) pow 2\r
 203          ==> (collinear {v1, v2, v3} <=> ups_x x12 x13 x23 = &0)`;;\r
 204 let lemma9 = FHFMKIY;;\r
 205 (* le 10. p 14 *)\r
 206 let ZPGPXNN =  `! v1 v2 (v:real^3).\r
 207          dist (v1,v2) < dist (v,v1) + dist (v,v2) ==> ~(v IN conv {v1, v2})`;;\r
 208 let lemma10 = ZPGPXNN;;\r
 209 (* le 11. p14 *)\r
 210 let FAFKVLR =  new_axiom ` ? t1 t2 t3. ! v1 v2 v3 (v:real^3).\r
 211    v IN ( affine hull {v1,v2,v3} ) /\\r
 212    ~collinear {v1, v2, v3} \r
 213              ==> v = t1 v1 v2 v3 v % v1 + t2 v1 v2 v3 v % v2 + t3 v1 v2 v3 v % v3 /\\r
 214                  t1 v1 v2 v3 v + t2 v1 v2 v3 v + t3 v1 v2 v3 v = &1 /\\r
 215                  (!ta tb tc. v = ta % v1 + tb % v2 + tc % v3\r
 216                     ==> ta = t1 v1 v2 v3 v /\\r
 217                         tb = t2 v1 v2 v3 v /\\r
 218                         tc = t3 v1 v2 v3 v )`;;\r
 219 \r
 220 let equivalent_lemma = prove(` (?t1 t2 t3.\r
 221          !v1 v2 v3 (v:real^N).\r
 222              v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}\r
 223              ==> v =\r
 224                  t1 v1 v2 v3 v % v1 + t2 v1 v2 v3 v % v2 + t3 v1 v2 v3 v % v3 /\\r
 225                  t1 v1 v2 v3 v + t2 v1 v2 v3 v + t3 v1 v2 v3 v = &1 /\\r
 226                  (!ta tb tc.\r
 227                       v = ta % v1 + tb % v2 + tc % v3\r
 228                       ==> ta = t1 v1 v2 v3 v /\\r
 229                           tb = t2 v1 v2 v3 v /\\r
 230                           tc = t3 v1 v2 v3 v))  <=>\r
 231      \r
 232           ( !v1 v2 v3 (v:real^N).\r
 233              v IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}\r
 234           ==> (?t1 t2 t3.\r
 235                    v = t1 % v1 + t2 % v2 + t3 % v3 /\\r
 236                    t1 + t2 + t3 = &1 /\\r
 237                    (!ta tb tc.\r
 238                         v = ta % v1 + tb % v2 + tc % v3\r
 239                         ==> ta = t1 /\ tb = t2 /\ tc = t3))) `,\r
 240 REWRITE_TAC[GSYM SKOLEM_THM; LEFT_FORALL_IMP_THM; RIGHT_EXISTS_IMP_THM]);;\r
 241 \r
 242 let lemma11 = REWRITE_RULE[equivalent_lemma] FAFKVLR;;\r
 243 (* let COEFS = new_specification ["coef1"; "coef2"; "coef3"] FAFKVLR;; *)\r
 244 let plane_3p = new_definition `plane_3p (a:real^3) b c =\r
 245          {x | ~collinear {a, b, c} /\\r
 246               (?ta tb tc. ta + tb + tc = &1 /\ x = ta % a + tb % b + tc % c)}`;;\r
 247 (* le 12. p 15 *)\r
 248 let CNXIFFC =  ` ! (v1:real^3) (v2:real^3) (v3:real^3) (v:real^3). ~ collinear {v1,v2,v3} /\ v IN affine hull \r
 249 {v1, v2, v3} \r
 250   ==> ( &0 < coef1 v1 v2 v3 v <=> v IN aff_gt {v2,v3} {v1} ) /\\r
 251   ( &0 = coef1 v1 v2 v3 v <=> v IN aff {v2,v3} ) /\\r
 252   ( coef1 v1 v2 v3 v < &0 <=> v IN aff_lt {v2,v3} {v1} ) /\\r
 253    ( &0 < coef2 v1 v2 v3 v <=> v IN aff_gt {v3,v1} {v2} ) /\\r
 254   ( &0 = coef2 v1 v2 v3 v <=> v IN aff {v3,v1} ) /\\r
 255   ( coef2 v1 v2 v3 v < &0 <=> v IN aff_lt {v3,v1} {v2} )/\\r
 256    ( &0 < coef3 v1 v2 v3 v <=> v IN aff_gt {v1,v2} {v3} ) /\\r
 257   ( &0 = coef3 v1 v2 v3 v <=> v IN aff {v1,v2} ) /\\r
 258   ( coef3 v1 v2 v3 v < &0 <=> v IN aff_lt {v1,v2} {v3})`;;\r
 259 let lemma12 = CNXIFFC;;\r
 260 (* le 13. p 15 *)\r
 261 let MYOQCBS =  ` ! v1 v2 v3 (v:real^3). ~ collinear {v1,v2,v3}/\\r
 262   v IN affine hull {v1,v2,v3} ==>\r
 263    ( v IN conv {v1,v2,v3} <=> &0 <= coef1 v1 v2 v3 v /\ &0 <= coef2 v1 v2 v3 v /\\r
 264    &0 <= coef3 v1 v2 v3 v ) /\ \r
 265    ( v IN conv0 {v1,v2,v3} <=> &0 < coef1 v1 v2 v3 v /\ &0 < coef2 v1 v2 v3 v /\\r
 266    &0 < coef3 v1 v2 v3 v )`;;\r
 267 let lemma13 = MYOQCBS;;\r
 268 (* le 14. p 15 *)\r
 269 \r
 270 let TXDIACY =  `! (a:real^3) b c d (v0: real^3) r.\r
 271  {a, b, c, d} SUBSET normball v0 r\r
 272          ==> convex hull {a, b, c, d} SUBSET normball v0 r `;;\r
 273 \r
 274 (* le 15. p 16 *)\r
 275 let POLFLZY =  ` ! x1 x2 x3 (x4: real^3).  \r
 276          let x12 = dist (x1,x2) pow 2 in\r
 277          let x13 = dist (x1,x3) pow 2 in\r
 278          let x14 = dist (x1,x4) pow 2 in\r
 279          let x23 = dist (x2,x3) pow 2 in\r
 280          let x24 = dist (x2,x4) pow 2 in\r
 281          let x34 = dist (x3,x4) pow 2 in\r
 282          coplanar {x1, x2, x3, x4} <=> delta x12 x13 x14 x23 x24 x34 = &0 `;;\r
 283 (* =============== *)\r
 284 (* ====  *   ===== *)\r
 285 (* ==   * *     == *)\r
 286 (*       *         *)\r
 287 (*    3 rd time    *)\r
 288 (* =============== *)\r
 289 \r
 290 (* le 16 *)\r
 291 let SDIHJZK = `! (v1:real^3) v2 v3 (a01: real) a02 a03.\r
 292          ~collinear {v1, v2, v3} /\\r
 293          (let x12 = d3 v1 v2 pow 2 in\r
 294           let x13 = d3 v1 v3 pow 2 in\r
 295           let x23 = d3 v2 v3 pow 2 in delta a01 a02 a03 x23 x13 x12 = &0)\r
 296          ==> (?!v0. a01 = d3 v0 v1 pow 2 /\\r
 297                     a02 = d3 v0 v2 pow 2 /\\r
 298                     a03 = d3 v0 v3 pow 2 /\\r
 299                     (let x12 = d3 v1 v2 pow 2 in\r
 300                      let x13 = d3 v1 v3 pow 2 in\r
 301                      let x23 = d3 v2 v3 pow 2 in\r
 302                      let vv = ups_x x12 x13 x23 in\r
 303                      let t1 = delta_x12 a01 a02 a03 x23 x13 x12 / vv in\r
 304                      let t2 = delta_x13 a01 a02 a03 x23 x13 x12 / vv in\r
 305                      let t3 = delta_x14 a01 a02 a03 x23 x13 x12 / vv in\r
 306                      v0 = t1 % v1 + t2 % v2 + t3 % v3))`;;\r
 307 \r
 308 (* le 17, p 17 *)\r
 309 let CDEUSDF =  `!(va:real^3) vb vc a b c.\r
 310      a = d3 vb vc /\ b = d3 va vc /\ c = d3 va vb /\ ~collinear {va, vb, vc}\r
 311      ==> (?p. p IN affine hull {va, vb, vc} /\\r
 312               (?c. !w. w IN {va, vb, vc} ==> c = dist (p,w)) /\\r
 313               (!p'. p' IN affine hull {va, vb, vc} /\\r
 314                     (?c. !w. w IN {va, vb, vc} ==> c = dist (p',w))\r
 315                     ==> p = p')) /\\r
 316          (let al_a =\r
 317               (a pow 2 * (b pow 2 + c pow 2 - a pow 2)) /\r
 318               (ups_x (a pow 2) (b pow 2) (c pow 2)) in\r
 319           let al_b =\r
 320               (b pow 2 * (a pow 2 + c pow 2 - b pow 2)) /\r
 321               (ups_x (a pow 2) (b pow 2) (c pow 2)) in\r
 322           let al_c =\r
 323               (c pow 2 * (a pow 2 + b pow 2 - c pow 2)) /\r
 324               (ups_x (a pow 2) (b pow 2) (c pow 2)) in\r
 325           al_a % va + al_b % vb + al_c % vc = circumcenter {va, vb, vc}) /\\r
 326          radV {va, vb, vc} = eta_y a b c`;;\r
 327 \r
 328 let CDEUSDF_CHANGE =  `!(va:real^3) vb vc a b c.\r
 329      a = d3 vb vc /\ b = d3 va vc /\ c = d3 va vb /\ ~collinear {va, vb, vc}\r
 330      ==> (?p. p IN affine hull {va, vb, vc} /\\r
 331               (?c. !w. w IN {va, vb, vc} ==> c = dist (p,w)) /\\r
 332               (!p'. p' IN affine hull {va, vb, vc} /\\r
 333                     (?c. !w. w IN {va, vb, vc} ==> c = dist (p',w))\r
 334                     ==> p = p')) /\\r
 335          (let al_a =\r
 336               (a pow 2 * (b pow 2 + c pow 2 - a pow 2)) /\r
 337               (ups_x (a pow 2) (b pow 2) (c pow 2)) in\r
 338           let al_b =\r
 339               (b pow 2 * (a pow 2 + c pow 2 - b pow 2)) /\r
 340               (ups_x (a pow 2) (b pow 2) (c pow 2)) in\r
 341           let al_c =\r
 342               (c pow 2 * (a pow 2 + b pow 2 - c pow 2)) /\r
 343               (ups_x (a pow 2) (b pow 2) (c pow 2)) in\r
 344           al_a % va + al_b % vb + al_c % vc = circumcenter {va, vb, vc}) /\\r
 345          radV {va, vb, vc} = eta_y a b c`;;\r
 346 (* le 18, p 17 *)\r
 347 let WSMRDKN =  `!x y z p.\r
 348          d3 x z pow 2 < d3 x y pow 2 + d3 y z pow 2 /\\r
 349          ~collinear {x, y, z} /\\r
 350          p = circumcenter {x, y, z}\r
 351          ==> p IN aff_gt {x, z} {y}  `;;\r
 352 \r
 353 \r
 354 (* le 19. p 17 *)\r
 355 let BYOWBDF = `! a b c a' b' ( c':real).\r
 356 &0 < a /\\r
 357          a <= a' /\\r
 358          &0 < b /\\r
 359          b <= b' /\\r
 360          &0 < c /\\r
 361          c <= c' /\\r
 362          a' pow 2 <= b pow 2 + c pow 2 /\\r
 363          b' pow 2 <= a pow 2 + c pow 2 /\\r
 364          c' pow 2 <= a pow 2 + b pow 2\r
 365          ==> eta_y a b c <= eta_y a' b' c' `;;\r
 366 \r
 367 (* le 20, p 18 *)\r
 368 let BFYVLKP =  ` ! x y z: real^3.\r
 369    &2 <= d3 x y /\\r
 370          d3 x y <= #2.52 /\\r
 371          &2 <= d3 x z /\\r
 372          d3 x z <= #2.2 /\\r
 373          &2 <= d3 y z /\\r
 374          d3 y z <= #2.2\r
 375          ==> ~collinear {x, y, z} /\ radV {x, y, z} < sqrt (&2)`;;\r
 376 (* le 21. p 18 *)\r
 377 let WDOMZXH = ` ! y. &2 <= y /\ y <= sqrt8 ==> eta_y y (&2) #2.51 < #1.453`;;\r
 378 (* le 22. p 18 *)\r
 379 let ZEDIDCF =  ` ! v0 v1 (v2:real^3).\r
 380          &2 <= d3 v0 v1 /\\r
 381          d3 v0 v1 <= #2.51 /\\r
 382          #2.45 <= d3 v1 v2 /\\r
 383          d3 v1 v2 <= #2.51 /\\r
 384          #2.77 <= d3 v0 v2 /\\r
 385          d3 v0 v2 <= sqrt8\r
 386          ==> sqrt2 < radV {v0, v1, v2}`;;\r
 387 (* le 23, p 19 *)\r
 388 let NHSJMDH =  ` ! y. #2.696 <= y /\ y <= sqrt8 ==>\r
 389      eta_y y (&2) (#2.51) <= eta_y y #2.45 (#2.45) `;;\r
 390 \r
 391 (* le 24 , p 19 *)\r
 392 let HVXIKHW =  ` ! x y z. &0 <= x /\ &0 <= y /\ &0 <= z /\ \r
 393           &0 < ups_x_pow2 x y z ==> max_real3 x y z / &2 <= eta_y x y z `;;\r
 394 (* le 25. p 19 *)\r
 395 let HMWTCNS =  ` ! a b (c:real^3). \r
 396              packing {a, b, c} /\ ~ collinear {a,b,c} \r
 397          ==> &2 / sqrt (&3) <= radV {a, b, c}`;;\r
 398 (* le 26 . p 20 *)\r
 399 let POXDVXO =  ` ! v1 v2 (v3:real^3) p.\r
 400          ~collinear {v1, v2, v3} /\\r
 401          p = circumcenter {v1, v2, v3}\r
 402          ==> (p - &1 / &2 % (v1 + v2)) dot (v1 - v2) = &0 /\\r
 403          ( p - &1 / &2 % ( v2 + v3 )) dot (v2 - v3 ) = &0 /\\r
 404          ( p - &1 / &2 % ( v3 + v1 )) dot ( v3 - v1 ) = &0 `;;\r
 405 (* le 27. p 20 *)\r
 406 let MAEWNPU = new_axiom ` ? b c. ! x12 x13 x14 x23 x24 x34.\r
 407   delta x12 x13 x14 x23 x24 x34 = -- x12 * ( x34  pow 2 ) + b x12 x13 x14 x23 x24 * x34 +\r
 408   c x12 x13 x14 x23 x24`;;\r
 409 \r
 410 let DELTA_COEFS = new_specification ["b_coef"; "c_coef"] MAEWNPU;;\r
 411 (* le 28. p 20 *)\r
 412 let AGBWHRD =  ` ! x12 x13 x14 x23 x24.\r
 413    !x12 x13 x14 x23 x24.\r
 414          b_coef x12 x13 x14 x23 x24 pow 2 +\r
 415          &4 * x12 * c_coef x12 x13 x14 x23 x24 =\r
 416          ups_x x12 x23 x13 * ups_x x12 x24 x14 `;;\r
 417 \r
 418 (* le 29 . p 21 *)\r
 419 let VCRJIHC = ` ! x34 x12 x13 v1 x14 v3 x23 v2 v4 x24.\r
 420   condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 ==>\r
 421   muy_delta x12 x13 x14 x23 x24 ( dist( v3,v4) pow 2 ) = &0 `;;\r
 422 (* le 30. p21 *)\r
 423 let EWVIFXW = ` !v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 a b c.\r
 424      condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 /\\r
 425      (!x12 x13 x14 x23 x24 x34.\r
 426           muy_delta x12 x13 x14 x23 x24 x34 =\r
 427           a x12 x13 x14 x23 x24 * x34 pow 2 +\r
 428           b x12 x13 x14 x23 x24 * x34 +\r
 429           c x12 x13 x14 x23 x24 )\r
 430      ==> (v3 IN aff {v1, v2} \/ v4 IN aff {v1, v2} <=>\r
 431           b x12 x13 x14 x23 x24 pow 2 -\r
 432           &4 * a x12 x13 x14 x23 x24 * c x12 x13 x14 x23 x24 =\r
 433           &0)`;;\r
 434 \r
 435 (* le 31. p 21 *)\r
 436 let FFBNQOB = ` !v1 v2 v3 v4 x12 x13 x14 x23 x24 x34. \r
 437         !v1 v2 v3 v4 x12 x13 x14 x23 x24 x34.\r
 438          condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 /\\r
 439          ~(conv {v3, v4} INTER affine hull {v1, v2} = {})\r
 440          ==> muy_delta x12 x13 x14 x23 x24 (dist (v3,v4) pow 2) = &0 /\\r
 441              (!root. muy_delta x12 x13 x14 x23 x24 root = &0\r
 442                      ==> root <= dist (v3,v4) pow 2) `;;\r
 443 (* le 32 . p 21 *)\r
 444 let CHHSZEO =  `!v1 v2 v3 v4 x12 x13 x14 x23 x24 x34.\r
 445          condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 /\\r
 446          conv {v3, v4} INTER affine hull {v1, v2} = {}\r
 447          ==> muy_delta x12 x13 x14 x23 x24 (dist (v3,v4) pow 2) = &0 /\\r
 448              (!root. muy_delta x12 x13 x14 x23 x24 root = &0\r
 449                      ==>dist (v3,v4) pow 2 <= root )`;;\r
 450 \r
 451 (* le 33. P 22 *)\r
 452 \r
 453 let CMUDPKT = ` !x34 x12 x13 v1 x14 v3 x23 v2 v4 x24 x34' x34'' a.\r
 454          condA v1 v2 v3 v4 x12 x13 x14 x23 x24 x34 /\ x34' <= x34'' /\\r
 455   (! x. muy_delta x12 x13 x14 x23 x24 x = a * ( x - x34' ) * ( x - x34'')) \r
 456   ==> delta_x34 x12 x13 x14 x23 x24 x34' =\r
 457              sqrt (ups_x x12 x13 x23 * ups_x x12 x14 x24) /\\r
 458              delta_x34 x12 x13 x14 x23 x24 x34' =\r
 459              --sqrt (ups_x x12 x13 x23 * ups_x x12 x14 x24) `;;\r
 460 \r
 461 (* le 34. p 22 *)\r
 462 let CXWOCGN = ` !M13 m12 m14 M24 m34 m23 (v1:real^3) v2 v3 v4.\r
 463          condC M13 m12 m14 M24 m34 m23 /\\r
 464   CARD {v1,v2,v3,v4} = 4 /\\r
 465   m12 <= d3 v1 v2 /\ \r
 466   m23 <= d3 v2 v3 /\\r
 467   m34 <= d3 v3 v4 /\ \r
 468   m14 <= d3 v1 v4 /\ \r
 469   d3 v1 v3 < M13 /\\r
 470   d3 v2 v4 <= M24 ==>\r
 471   conv {v1,v3} INTER conv {v2,v4} = {} `;;\r
 472 \r
 473 (* le 35. p 22 *)\r
 474 let THADGSB = ` !M13 m12 m14 M24 m34 m23 v1 v2 v3 v4.\r
 475          (!x. x IN {M13, m12, m14, M24, m34, m23} ==> &0 <= x) /\\r
 476          M13 < m12 + m23 /\\r
 477          M13 < m14 + m34 /\\r
 478          M24 < m12 + m14 /\\r
 479          M24 < m23 + m34 /\\r
 480          &0 <\r
 481          delta (M13 pow 2) (m12 pow 2) (m14 pow 2) (M24 pow 2) (m34 pow 2)\r
 482          (m23 pow 2) /\\r
 483          CARD {v1, v2, v3, v4} = 4 /\ \r
 484    m12 <= d3 v1 v2 /\\r
 485          m23 <= d3 v2 v3 /\\r
 486          m34 <= d3 v3 v4 /\\r
 487          m14 <= d3 v1 v4 /\\r
 488          d3 v1 v3 <= M13 /\\r
 489          d3 v2 v4 <= M24 ==> conv {v1,v3} INTER conv {v2,v4} = {} `;;\r
 490 (* le 36. p 23 *)\r
 491 let ZZSBSIO = ` ! u v w. CARD {u,v,w} = 3 /\ packing {u,v,w} /\\r
 492   dist (u,v) < sqrt8 ==>  dist (u,v) / &2 < dist (w, &1 / &2 % ( u + v )) `;;\r
 493 \r
 494 (* le 37. p24 *)\r
 495 let JGYWWBX =  ` ~ (?v1 v2 w1 (w2:real^3).\r
 496            CARD {v1, v2, w1, w2} = 4 /\\r
 497            packing {v1, v2, w1, w2} /\\r
 498            dist (v1,w2) >= sqrt8 /\\r
 499            dist (v1,v2) <= #3.2 /\\r
 500            dist (w1,w2) <= sqrt8 /\\r
 501            ~(conv {v1, v2} INTER conv {w1, w2} = {}))`;;\r
 502 (* le 38. p 24 *)\r
 503 let PAHFWSI = ` !(v1:real^3) v2 v3 v4.\r
 504          CARD {v1, v2, v3, v4} = 4 /\\r
 505          packing {v1, v2, v3, v4} /\\r
 506          dist (v1,v3) <= #3.2 /\\r
 507          #2.51 <= dist (v1,v2) /\\r
 508          dist (v2,v4) <= #2.51\r
 509          ==> conv {v1, v3} INTER conv {v2, v4} = {} `;;\r
 510 (* le 39. p 24 *)\r
 511 let UVGVIXB =  ` ! (v1:real^3) v2 w1 w2.\r
 512          CARD {v1, v2, w1, w2} = 4 /\\r
 513          packing {v1, v2, w1, w2} /\\r
 514          dist (w1,w2) <= #2.51 /\\r
 515          dist (v1,v2) <= #3.07\r
 516          ==> conv {w1, w2} INTER conv {v1, v2} = {}`;;\r
 517 (* le 40 . p 25 *)\r
 518 let PJFAYXI = ` ! (v1:real^3) v2 w1 w2.\r
 519  CARD {v1, v2, w1, w2} = 4 /\\r
 520          packing {v1, v2, w1, w2} /\\r
 521          dist (v1,v2) <= #3.2 /\\r
 522          dist (w1,w2) <= #2.51 /\\r
 523          #2.2 <= dist (v1,w1)\r
 524          ==> conv {v1, v2} INTER conv {w1, w2} = {}`;;\r
 525 (* le 41. p 25 *)\r
 526 let YXWIPMH =  ` ! v1 v2 v3 (v4:real^3).\r
 527  CARD {v1,v2,v3,v4} = 4 /\ \r
 528  d3 v1 v2 = #2.51 /\\r
 529          d3 v1 v3 = &2 /\\r
 530          d3 v1 v4 = &2 /\\r
 531          d3 v2 v3 = &2 /\\r
 532          d3 v2 v4 = &2\r
 533          ==> d3 v3 v4 <= #3.114467 `;;\r
 534 (* le 42. p 25 *)\r
 535 let PAATDXJ =  ` ! v1 v2 v3 (v4:real^3).\r
 536          CARD {v1,v2,v3,v4} = 4 /\ \r
 537          d3 v1 v2 = #2.51 /\\r
 538          d3 v1 v4 = #2.51 /\\r
 539          d3 v2 v3 = &2 /\\r
 540          d3 v3 v4 = &2 /\\r
 541          sqrt8 <= d3 v2 v4\r
 542          ==> d3 v1 v3 < #3.488 `;;\r
 543 \r
 544 (* le 43 . p 26 *)\r
 545 let YJHQPAL =  `\r
 546 !m14 m24 m34 M23 M13 M12.\r
 547          condF m14 m24 m34 M23 M13 M12\r
 548          ==> ~(?v1 v2 v3 v4.\r
 549                    coplanar {v1, v2, v3, v4} /\\r
 550                    v4 IN conv {v1, v2, v3} /\\r
 551                    (let y12 = d3 v1 v2 in\r
 552                     let y13 = d3 v1 v3 in\r
 553                     let y14 = d3 v1 v4 in\r
 554                     let y23 = d3 v2 v3 in\r
 555                     let y24 = d3 v2 v4 in\r
 556                     let y34 = d3 v3 v4 in\r
 557                     m14 <= y14 /\\r
 558                     m24 <= y24 /\\r
 559                     m34 <= y34 /\\r
 560                     y23 <= M23 /\\r
 561                     y13 <= M13 /\\r
 562                     y12 <= M12))`;;\r
 563 (* le 44 . p 27 *)\r
 564 let MPXSJDI = ` !m M13 M23 m34. condS m m34 M13 M23\r
 565      ==> ~(?v1 v2 v3 v4.\r
 566                coplanar {v1, v2, v3, v4} /\\r
 567                v4 IN conv {v1, v2, v3} /\\r
 568                m <= d3 v1 v4 /\\r
 569                m <= d3 v2 v4 /\\r
 570                m34 <= d3 v3 v4 /\\r
 571                d3 v2 v3 <= M23 /\\r
 572                d3 v1 v3 <= M13)`;;\r
 573 (* le 45. p 30 *)\r
 574 \r
 575 let VMZBXSQ = ` !v0 v1 v2 (v3: real^3).\r
 576      packing {v0, v1, v2, v3} /\\r
 577      CARD {v0, v1, v2, v3} = 4 /\\r
 578      d3 v0 v1 <= #2.51 /\\r
 579      d3 v0 v2 <= #2.51 /\\r
 580      d3 v0 v3 <= #2.51 /\\r
 581      d3 v1 v2 <= #3.2 /\\r
 582      #2.51 <= d3 v1 v3\r
 583      ==> rcone_gt v0 v3 (d3 v0 v3 / #2.51) INTER cone v0 {v1, v2} = {}`;;\r
 584 let LEMMA45 = VMZBXSQ;;\r
 585 (* le 46 . p 31 *)\r
 586 let QNXDWNU = ` !v0 v1 v2 (v3:real^3).\r
 587      packing {v0, v1, v2, v3} /\\r
 588      CARD {v0, v1, v2, v3} = 4 /\\r
 589      d3 v0 v2 <= #2.23 /\\r
 590      d3 v0 v3 <= #2.23 /\\r
 591      #2.77 <= d3 v2 v3 /\\r
 592      d3 v2 v3 <= sqrt8 /\\r
 593      (!x. x IN {v0, v2, v3} ==> d3 v1 x <= #2.51)\r
 594      ==> rcone_gt v0 v1 (d3 v0 v1 / #2.77) INTER cone v0 {v2, v3} = {}`;;\r
 595 let LEMMA46 = QNXDWNU ;;\r
 596 (* le 47. p 32 *)\r
 597 let PNUMEHN = `! v0 v1 v2 (v3 :real^3). packing {v0,v1,v2,v3} /\ \r
 598   #2.51 <= d3 v1 v2 /\ #2.51 <= d3 v1 v3 /\\r
 599   d3 v2 v3 <= #3.2 ==>\r
 600   let y = d3 v0 v1 in\r
 601   let h = cos_arc y ( #1.255 ) ( #1.6 ) in\r
 602   cone v0 {v2,v3} INTER rcone_gt v0 v1 h = {} `;;\r
 603 let LEMAA47 = PNUMEHN ;;\r
 604 \r
 605 (* le 48 . p 33 *)\r
 606 let HLAHAUS = ` !v0 v1 v2 (v3:real^3).\r
 607      packing {v0, v1, v2, v3} /\\r
 608      d3 v1 v2 = &2 /\\r
 609      #3.2 <= d3 v1 v3 /\\r
 610      d3 v2 v3 <= #3.2 /\\r
 611      ( let y = d3 v0 v1 in\r
 612       #2.2 <= y /\ y <= #2.51 )\r
 613       ==> (let y = d3 v0 v1 in\r
 614            let h = cos_arc y #2.255 #1.6 in\r
 615            cone v0 {v2, v3} INTER rcone_gt v0 v1 h = {})`;;\r
 616 (* le 49 . p 33 *)\r
 617 \r
 618 let RISDLIH = ` ! v0 v1 v2 (v3:real^3). d3 v0 v2 <= #2.51 /\\r
 619      d3 v0 v3 <= #2.51 /\\r
 620      d3 v1 v2 = &2 /\\r
 621      #3.2 <= d3 v1 v3 /\\r
 622      (let y = d3 v0 v1 in\r
 623       &2 <= y /\ y <= #2.2 /\ d3 v2 v3 <= #3.2 ) \r
 624       ==> ((let y = d3 v0 v1 in let h = cos_arc y #1.255 #1.6 in h = &1))`;;\r
 625 (* ====================== *)\r
 626 \r
 627 (* lemma 50. p 34 *)\r
 628 \r
 629 let LTCTBAN = `! x12 x13 x14 x15 x23 x24 x25 x34 x35 x45.\r
 630  cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 = \r
 631 ups_x x12 x13 x23 * x45 pow 2 + cayleytr x12 x13 x14 x15 x23 x24 x25 x34 x35 ( &0 )\r
 632 * x45 + cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 ( &0 ) `;;\r
 633 (* lemma 51. p 34 *)\r
 634 let GJWYYPS = `!x12 x13 x14 x15 x23 x24 x25 x34 x35 a b c.\r
 635     (! x45.  cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =\r
 636      a  * x45 pow 2 + b * x45 + c )\r
 637      ==> b pow 2 - &4 * a * c =\r
 638          &16 * delta x12 x13 x14 x23 x24 x34 * delta x12 x13 x15 x23 x25 x35`;;\r
 639 \r
 640 (* le 52 *)\r
 641 let PFDFWWV =  ` ! v1 v2 v3 v4 (v5:real^3).\r
 642   muy_v v1 v2 v3 v4 v5 ( (d3 v4 v5) pow 2 ) = &0 `;;\r
 643 (* le 53 .p 35 *)\r
 644 let GDLRUZB =  `!v1 v2 v3 v4 v5 a b c.\r
 645          coplanar {v1, v2, v3, v4} \/ coplanar {v1, v2, v3, v5} <=>\r
 646          (!a b c.\r
 647               (!x. muy_v v1 v2 v3 v4 v5 x = a * x pow 2 + b * x + c)\r
 648               ==> b pow 2 - &4 * a * c = &0)`;;\r
 649 (* le 54. p 35 *)\r
 650 let KGSNYDS =  `! v1 v2 v3 v4 (v5:real^3).\r
 651   ~ collinear {v1,v2,v3} /\ conv {v4,v5} INTER affine hull {v1,v2,v3} = {} \r
 652  ==> muy_v v1 v2 v3 v4 v5 (( d3 v4 v5) pow 2 )  = &0 /\\r
 653    (! x. muy_v v1 v2 v3 v4 v5 x = &0 ==>\r
 654    x <= ( d3 v4 v5) pow 2 ) `;;\r
 655 (* le 55. p 36 *)\r
 656 let KGSNYDS =  `! v1 v2 v3 v4 (v5:real^3).\r
 657   ~ collinear {v1,v2,v3} /\ ~ (conv0 {v4,v5} INTER affine hull {v1,v2,v3} = {} )\r
 658  ==> muy_v v1 v2 v3 v4 v5 (( d3 v4 v5) pow 2 )  = &0 /\\r
 659    (! x. muy_v v1 v2 v3 v4 v5 x = &0 ==>\r
 660     d3 v4 v5 pow 2 <= x )`;;\r
 661 (* le 56. p 36 *)\r
 662 let QHSEWMI =  `!v1 v2 v3 w1 w2.\r
 663      ~(conv {w1, w2} INTER conv {v1, v2, v3} = {}) /\\r
 664      ~(w1 IN conv {v1, v2, v3})\r
 665      ==> w2 IN cone w1 {v1, v2, v3}`;;\r
 666 (* lemma 57. p 36 *)\r
 667 let LEMMA57 =  ` !v1 v2 v3 w1 (w2: real^3).\r
 668      packing {v1, v2, v3, w1, w2} /\\r
 669      CARD {v1, v2, v3, w1, w2} = 5 /\\r
 670      ~collinear {v1, v2, v3} /\\r
 671      radV {v1, v2, v3} < sqrt2 /\\r
 672      d3 w1 w2 < sqrt8\r
 673      ==> conv {v1, v2, v3} INTER conv {w1, w2} = {}`;;\r
 674 let DOUFCOI = LEMMA57;;\r
 675 \r
 676 \r
 677 let LEMMA58 =  `! m12 m13 m14 m25 m35 m45 M23 M34 M24 M15.\r
 678   (!x. x IN {m12, m13, m14, m25, m35, m45, M23, M34, M24, M15}\r
 679               ==> &0 <= x) /\\r
 680          condC M15 m12 m13 M23 m35 m25 /\\r
 681          condC M15 m13 m14 M34 m45 m35 /\\r
 682          condC M15 m12 m24 M24 m45 m25 /\\r
 683          condF m25 m35 m45 M34 M24 M23 /\\r
 684          condF m12 m13 m14 M34 M24 M23 /\\r
 685          M15 < sqrt_of_ge_root m12 m13 m14 M34 M24 M23 m25 m35 m45\r
 686          ==> ~(?(v1:real^3) v2 v3 v4 v5.\r
 687                    CARD {v11, v2, v3, v4, v5} = 5 /\\r
 688                    ~collinear {v2, v3, v4} /\\r
 689                    ~(conv {v1, v5} INTER conv {v2, v3, v4} = {}) /\\r
 690   (let x12 = dist (x1,x2) in\r
 691                     let x13 = dist (x1,x3) in\r
 692                     let x14 = dist (x1,x4) in\r
 693                     let x15 = dist (x1,x5) in\r
 694                     let x23 = dist (x2,x3) in\r
 695                     let x24 = dist (x2,x4) in\r
 696                     let x25 = dist (x2,x5) in\r
 697                     let x34 = dist (x3,x4) in\r
 698                     let x35 = dist (x3,x5) in\r
 699                     let x45 = dist (x4,x5) in\r
 700                     x15 <= M15 /\\r
 701                     x23 <= M23 /\\r
 702                     x24 <= M24 /\\r
 703                     x34 <= M34 /\\r
 704                     x12 >= m12 /\\r
 705                     x13 >= m13 /\\r
 706                     x14 >= m14 /\\r
 707                     x25 >= m25 /\\r
 708                     x35 >= m35 /\\r
 709                     x45 >= m45)) `;;\r
 710 let UQQVJON = LEMMA58;;\r
 711 \r
 712 \r
 713 \r
 714 (* lemma 59. p 36 *)\r
 715 let LEMMA59 =  ` !v1 v2 v3 v4 ( v5:real^3).\r
 716          packing {v1, v2, v3, v4, v5} /\\r
 717          CARD {v1, v2, v3, v4,v5} = 5 /\\r
 718          d3 v2 v3 <= #2.52 /\\r
 719          d3 v3 v4 <= #2.52 /\\r
 720          d3 v4 v2 <= #2.52 /\\r
 721          d3 v1 v5 <= sqrt8 /\\r
 722          ~(conv {v1, v5} INTER conv {v2, v3, v4} = {})\r
 723          ==> (!aa bb.\r
 724                   aa IN {v1, v5} /\ bb IN {v2, v3, v4} ==> d3 aa bb <= #2.2)`;;\r
 725 let FRCXQKB = LEMMA59 ;;\r
 726 (* lemma 60 , p 38 *)\r
 727 let LEMMA60 =  `!v0 v1 v2 v3 v4.\r
 728      packing {v1, v2, v3, v4, v0} /\\r
 729      CARD {v1, v2, v3, v4, v0} = 5 /\\r
 730      (!x. x IN {v1, v2, v3, v4} ==> d3 v0 x <= #2.51) /\\r
 731      d3 v1 v3 <= #2.51 /\\r
 732      d3 v2 v4 <= #2.51\r
 733      ==> {v0} = cone v0 {v1, v3} INTER cone v0 {v1, v4}`;;\r
 734 let ZHBBLXP = LEMMA60 ;;\r
 735 (* le 62. p 40 *)\r
 736 let LEMMA62 = ` ! v0 v1 v2 v (w:real^3).\r
 737   ~ ( CARD {v0, v1, v2, v, w} = 5 /\\r
 738          ~(conv {v, w} INTER cone v0 {v1, v2} = {}) /\\r
 739          (!u. u IN {v1, v2, v, w} ==> &2 <= d3 u v0 /\ d3 u v0 <= #2.51) /\\r
 740          #3.2 <= d3 v v1 /\\r
 741          &2 <= d3 v v2 /\\r
 742          &2 <= d3 w v2 /\\r
 743          &2 <= d3 w v1 /\\r
 744          d3 v w <= #2.2 /\\r
 745          &2 <= d3 v2 v1 /\\r
 746          d3 v1 v2 <= #3.2  ) `;;\r
 747 let VNZLYWT = LEMMA62;;\r
 748 (* le 63. p 42 *)\r
 749 let LEMMA63 = ` ! v0 v1 v2 v3 (w:real^3).\r
 750 CARD {v0, v1, v2, v3, w} = 5 /\\r
 751          #2.51 <= d3 w v0 /\\r
 752          d3 w v0 <= sqrt8 /\\r
 753          d3 v1 v3 <= sqrt8 /\\r
 754          (!u. u IN {v0, v1, v2, v3, w} ==> d3 u v0 <= #2.51) /\\r
 755          ~(conv {v1, v3} INTER conv {v0, w, v2} = {})\r
 756          ==> min (d3 v1 v2) (d3 v2 v3) <= #2.51 /\\r
 757              (min (d3 v1 v2) (d3 v2 v3) = #2.51\r
 758               ==> d3 v1 v2 = #2.51 /\ d3 v2 v3 = two_t0) `;;\r
 759 let VAXNRNE = LEMMA62;;\r
 760 (* le 64. p 42 *)\r
 761 let LEMMA64 = `! v0 v1 v2 v3 (v4:real^3).\r
 762   CARD {v0, v1, v2, v3, v4} = 5 /\\r
 763          (!u v. u IN {v0, v2} /\ v IN {v1, v3, v4} ==> d3 u v <= two_t0) /\\r
 764          d3 v1 v3 <= sqrt8 /\\r
 765          d3 v0 v2 <= sqrt8 /\\r
 766          ~(conv {v1, v3} INTER conv {v0, v2, v4} = {})\r
 767          ==> d3 v1 v4 <= #3.2`;;\r
 768 let GMOKOTN = LEMMA64;;\r
 769 (* le 65. p 43 *)\r
 770 let LEMMA65 =  ` ! v0 v1 v2 (v3:real^3).\r
 771   CARD {v0, v1, v2, v3} = 4 /\\r
 772          d3 v0 v1 <= two_t0 /\\r
 773          twp_t0 <= d3 v1 v2 /\\r
 774          (?a b c.\r
 775               {a, b, c} = {v0, v2, v3} /\\r
 776               d3 a b <= two_t0 /\\r
 777               d3 b c <= two_t0 /\\r
 778               d3 a c <= sqrt8)\r
 779          ==> rcone_gt v0 v1 (d3 v0 v1 / sqrt8) INTER cone v0 {v2, v3} = {} `;;\r
 780 let EFXWFNQ = LEMMA65;;\r
 781 (* lemma 66. p 43 *)\r
 782 let LEMMA66 =  ` ! v1 v2 v3 (v0:real^3).\r
 783   CARD {v0, v1, v2, v3} = 4 /\\r
 784          packing {v0, v1, v2, v3} /\\r
 785          d3 v1 v2 <= #2.51 /\\r
 786          d3 v2 v3 <= #2.51 /\\r
 787          d3 v1 v3 <= sqrt8 /\\r
 788          ~(normball v0 (sqrt (&2)) INTER conv {v1, v2, v3} = {})\r
 789          ==> (!x. x IN {v1, v2, v3} ==> d3 v0 x <= #2.51) `;;\r
 790 let LOKDUSSU = LEMMA66 ;;\r
 791 \r
 792 (* le 67. p 44 *)\r
 793 let LEMMA67 =  ` ! v1 v2 v3 (v0:real^3).\r
 794   CARD {v0, v1, v2, v3} = 4 /\\r
 795          packing {v0, v1, v2, v3} /\\r
 796          d3 v1 v2 <= #2.51 /\\r
 797          d3 v2 v3 <= #2.51 /\\r
 798          d3 v1 v3 <= sqrt8 ==>\r
 799 normball vo ( #1.255 ) INTER conv {v1,v2,v3} = {} `;;\r
 800 let FFSXOWD = LEMMA67 ;;\r
 801 \r
 802 (* le 68 . p 44 *)\r
 803 \r
 804 \r
 805 let LEMMA68 =  ` ! v v1 v2 v3 (v4:real^3).\r
 806 CARD {v, v1, v2, v3, v4} = 5 /\\r
 807          packing {v1, v2, v3, v4, v} /\\r
 808          (!x y. {x, y} SUBSET {v1, v2, v3, v4} ==> d3 x y <= sqrt8)\r
 809          ==> ~(v IN conv {v1, v2, v3, v4}) `;;\r
 810 let ZODWCKJ = LEMMA68 ;;\r
 811 \r
 812 (* le 69 . p45 *)\r
 813 \r
 814 let LEMMA69 =  ` ! v v1 v2 v3 (v4:real^3).\r
 815 CARD {v, v1, v2, v3, v4} = 5 /\\r
 816          packing {v1, v2, v3, v4, v} /\\r
 817  (!x y. {x, y} SUBSET {v1, v2, v3, v4} /\ ~ ( {x,y} = {v1,v2} ) ==> d3 x y < sqrt8)\r
 818 ==> ~ ( v IN conv {v1,v2,v3,v4} ) `;;\r
 819 let KCGHSFF = LEMMA69 ;;\r
 820 \r
 821 (* le 70. p 45 *)\r
 822 \r
 823 \r
 824 let LEMMA70 =  ` ! v5 v1 v2 v3 (v4:real^3).\r
 825 CARD {v5, v1, v2, v3, v4} = 5 /\\r
 826          packing {v1, v2, v3, v4, v5} /\\r
 827          (!x y.\r
 828               {x, y} SUBSET {v1, v2, v3, v4, v5} /\ ~({x, y} = {v1, v4})\r
 829               ==> d3 x y <= sqrt8)\r
 830          ==> ~(v5 IN conv {v1, v2, v3, v4}) `;;\r
 831 let TEAULMK = LEMMA70 ;;\r
 832  (* le 71 , p 46 *)\r
 833 let LEMMA71 =  ` ! w v v0 v1 (v2:real^3).\r
 834    let t = #2.51 in\r
 835          CARD {w, v, v0, v1, v2} = 5 /\\r
 836          packing {w, v, v0, v1, v2} /\\r
 837          d3 v v1 <= t /\\r
 838          d3 v v2 <= t /\\r
 839          d3 v0 v1 <= t /\\r
 840          d3 v0 v2 <= t /\\r
 841          d3 v0 v <= sqrt8 /\\r
 842          t <= d3 v0 w /\\r
 843          d3 v0 w <= sqrt8 /\\r
 844          w IN cone v0 {v1, v2, v}\r
 845          ==> d3 w v <= t `;;\r
 846 let EIYPZVL = LEMMA71;;\r
 847 (* le 72. p 47 *)\r
 848 let LEMMA72 = ` ! w v1 v2 v3 (v4:real^3). \r
 849   CARD {w, v1, v2, v3, v4} = 5 /\\r
 850          packing {w, v1, v2, v3, v4} /\\r
 851          (let t = #2.51 in\r
 852           d3 v2 v3 <= t /\\r
 853           d3 v3 v4 <= t /\\r
 854           d3 v2 v4 <= t /\\r
 855           t <= d3 v1 v2 /\\r
 856           t <= d3 v1 v3 /\\r
 857           d3 v1 v4 <= t /\\r
 858           d3 v1 w <= sqrt8 /\\r
 859           d3 v1 v2 <= sqrt8 /\\r
 860           d3 v1 v3 <= sqrt8)\r
 861          ==> ~(w IN cone v1 {v2, v3, v4}) `;;\r
 862 let VZETXZC = LEMMA72 ;;\r
 863 (* le 73 . p 47 *)\r
 864 let LEMMA73 =  ` ! v1 v2 v3 (v4:real^3) a01 a02 a03 .\r
 865   let x12 = d3 v1 v2 pow 2 in\r
 866          let x13 = d3 v1 v3 pow 2 in\r
 867          let x23 = d3 v2 v3 pow 2 in\r
 868          CARD {v1, v2, v3, v4} = 4 /\\r
 869          packing {v1, v2, v3, v4} /\\r
 870          ~coplanar {v1, v2, v3, v4} /\\r
 871   &0 <= a01 /\ &0 <= a02 /\ &0 <= a03 /\ \r
 872   delta a01 a02 a03 x12 x13 x23 >= &0\r
 873          ==> (?v0. v0 IN aff_ge {v1, v2, v3} {v4} /\\r
 874                    d3 v0 v1 pow 2 = a01 /\\r
 875                    d3 v0 v2 pow 2 = a02 /\\r
 876                    d3 v0 v3 pow 2 = a03 /\\r
 877                    (!vv0. vv0 IN aff_ge {v1, v2, v3} {v4} /\\r
 878                           d3 vv0 v1 pow 2 = a01 /\\r
 879                           d3 vv0 v2 pow 2 = a02 /\\r
 880                           d3 vv0 v3 pow 2 = a03\r
 881                           ==> vv0 = v0) /\\r
 882                    ( v0 IN aff {v1,v2,v3} <=> \r
 883                      delta a01 a02 a03 x12 x13 x23 = &0 )) `;;\r
 884 (* le 74 . p 48 *)\r
 885 let LFYTDXC = new_axiom ` ? p. ! v1 v2 v3 (v4:real^3) r.\r
 886   let s = {v1, v2, v3, v4} in\r
 887          CARD s = 4 /\\r
 888          packing s /\\r
 889          ~coplanar s /\\r
 890          eta_y (d3 v1 v2 pow 2) (d3 v1 v3 pow 2) (d3 v2 v3 pow 2) <= r\r
 891          ==> p v1 v2 v3 v4 r IN aff_ge {v1, v2, v3} {v4} /\\r
 892                    r = d3 ( p v1 v2 v3 v4 r ) v1 /\\r
 893                    r = d3 ( p v1 v2 v3 v4 r ) v2 /\\r
 894                    r = d3 ( p v1 v2 v3 v4 r )  v3 /\\r
 895                    (!w. w IN aff_ge {v1, v2, v3} {v4} /\\r
 896                         r = d3 w v1 /\\r
 897                         r = d3 w v2 /\\r
 898                         r = d3 w v3\r
 899                         ==> w = ( p v1 v2 v3 v4 r ) ) `;;\r
 900 \r
 901 let LEMMA74 = LFYTDXC;;\r
 902 let point_eq = new_specification ["point_eq"] LFYTDXC;;\r
 903 \r
 904 \r
 905 (* le 75 . p 48 *)\r
 906 let LEMMA75 = ` !v1 v2 v3 (v4:real^3) r p p' u. let s = {v1,v2,v3,v4} in\r
 907 let x12 = d3 v1 v2 pow 2 in\r
 908 let x13 = d3 v1 v3 pow 2 in\r
 909 let x23 = d3 v2 v3 pow 2 in\r
 910 ~ coplanar s /\\r
 911 CARD s = 4 /\\r
 912 eta_y x12 x13 x23 < r /\\r
 913 p' = point_eq v1 v2 v3 v4 r /\\r
 914 p = circumcenter {v1,v2,v3} /\ u IN aff {v1,v2,v3} ==>\r
 915 ( p' - p ) dot ( u - p ) = &0 `;;\r
 916 let TIEEBHT = LEMMA75;;\r
 917 \r
 918 (* le 76 . p49 *)\r
 919 let LEMMA76 = new_axiom` ?t1 t2 t3 t4.\r
 920      !v1 v2 v3 v4 (v: real^3).\r
 921          ~coplanar {v1, v2, v3, v4}\r
 922          ==> t1 v1 v2 v3 v4 v +\r
 923              t2 v1 v2 v3 v4 v +\r
 924              t3 v1 v2 v3 v4 v +\r
 925              t4 v1 v2 v3 v4 v =\r
 926              &1 /\\r
 927              v =\r
 928              t1 v1 v2 v3 v4 v % v1 +\r
 929              t2 v1 v2 v3 v4 v % v2 +\r
 930              t3 v1 v2 v3 v4 v % v3 +\r
 931              t4 v1 v2 v3 v4 v % v4 /\\r
 932              (!ta tb tc td.\r
 933                   v = ta % v1 + tb % v2 + tc % v3 + td % v4 /\\r
 934                   ta + tb + tc + td = &1\r
 935                   ==> ta = t1 v1 v2 v3 v4 v /\\r
 936                       tb = t2 v1 v2 v3 v4 v /\\r
 937                       tc = t3 v1 v2 v3 v4 v /\\r
 938                       td = t4 v1 v2 v3 v4 v) `;;\r
 939 let ECSEVNC = LEMMA76 ;;\r
 940 let COEFS_4 = new_specification ["COEF4_1"; "COEF4_2"; "COEF4_3"; "COEF4_4"] ECSEVNC ;;\r
 941 \r
 942 (* le 77. p 49 *)let LEMMA77 = ` ! v1 v2 v3 v4 (v:real^3).\r
 943   ~ coplanar {v1,v2,v3,v4} ==>\r
 944   ( COEF4_1 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v3, v4} {v1} ) /\\r
 945   ( COEF4_1 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v3,v4} ) /\\r
 946   ( COEF4_1 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v3,v4} {v1} ) /\\r
 947   ( COEF4_2 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v1,v3, v4} {v2} ) /\\r
 948   ( COEF4_2 v1 v2 v3 v4 v = &0 <=> v IN aff {v1,v3,v4} ) /\\r
 949   ( COEF4_2 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v1,v3,v4} {v2} ) /\  \r
 950   ( COEF4_3 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v4} {v3} ) /\\r
 951   ( COEF4_3 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v4} ) /\\r
 952   ( COEF4_3 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v4} {v3} )/\  \r
 953   ( COEF4_4 v1 v2 v3 v4 v < &0 <=> v IN aff_lt {v2,v1, v3} {v4} ) /\\r
 954   ( COEF4_4 v1 v2 v3 v4 v = &0 <=> v IN aff {v2,v1,v3} ) /\\r
 955   ( COEF4_4 v1 v2 v3 v4 v > &0 <=> v IN aff_gt {v2,v1,v3} {v4} )`;;\r
 956 \r
 957 (* le 78 . p 50 *)\r
 958 let LEMMA78 = ` ! v1 v2 v3 v4 (v:real^3).\r
 959   ~coplanar {v1, v2, v3, v4}\r
 960          ==> (v IN conv {v1, v2, v3, v4} <=>\r
 961               &0 <= COEF4_1 v1 v2 v3 v4 v /\\r
 962               &0 <= COEF4_2 v1 v2 v3 v4 v /\\r
 963               &0 <= COEF4_3 v1 v2 v3 v4 v /\\r
 964               &0 <= COEF4_4 v1 v2 v3 v4 v) /\\r
 965              (v IN conv0 {v1, v2, v3, v4} <=>\r
 966               &0 < COEF4_1 v1 v2 v3 v4 v /\\r
 967               &0 < COEF4_2 v1 v2 v3 v4 v /\\r
 968               &0 < COEF4_3 v1 v2 v3 v4 v /\\r
 969               &0 < COEF4_4 v1 v2 v3 v4 v) `;;\r
 970 let ZRFMKPY = LEMMA78;;\r
 971 \r
 972 \r
 973 (* le 79 . p 50 *)\r
 974 let LEMMA79 = ` ! v0 v1 v2 v3 (v4:real^3).\r
 975   let tt = #2.51 in\r
 976          let ss = sqrt (&8) in\r
 977          CARD {v0, v1, v2, v3, v4} = 5 /\\r
 978          packing {v1, v2, v3, v4, v0} /\\r
 979          (!v. v IN {v2, v3, v4} ==> d3 v1 v <= #2.51 /\ &2 <= d3 v1 v) /\\r
 980          tt < d3 v1 v0 /\\r
 981          d3 v1 v0 < ss /\\r
 982   d3 v0 v3 <= tt /\\r
 983   d3 v2 v4 <= tt /\\r
 984   d3 v0 v4 < ss /\\r
 985   d3 v0 v2 < ss /\\r
 986   ~(  tt < d3 v0 v2 /\ tt < d3 v0 v4 ) \r
 987   ==> ~ ( v3 IN aff_ge {v0,v1} {v2,v4} ) `;;\r
 988 \r
 989 let COEBRMF = LEMMA79 ;;\r
 990 \r
 991 (* le 80. p 51 *)\r
 992 let LEMMA80 = ` ! v0 v1 v2 v3 (v4:real^N).\r
 993    CARD {v0, v1, v2, v3, v4} = 5 /\\r
 994          (?x. ~(x = v0) /\ x IN cone v0 {v1, v3} INTER cone v0 {v2, v4})\r
 995          ==> ~(conv {v1, v3} INTER cone v0 {v2, v4} = {} /\\r
 996                conv {v2, v4} INTER cone v0 {v1, v3} = {})`;;\r
 997 let JVDAFRS = LEMMA80;;\r
 998 \r
 999 let LEMMA81 = ` ! v1 v2 v3 (v4:real^3).\r
1000   let s = {v1,v2,v3,v4} in\r
1001   CARD s = 4 /\ ~ coplanar s ==>\r
1002   conv s = aff_ge ( s DIFF {v1} ) {v1} INTER \r
1003   aff_ge ( s DIFF {v2} ) {v2} INTER \r
1004   aff_ge ( s DIFF {v3} ) {v3} INTER \r
1005   aff_ge ( s DIFF {v4} ) {v4} `;;\r
1006 let ARIKWRQ = LEMMA81 ;;\r
1007 \r
1008 (* le 82. p 52 *)\r
1009 let LEMMA82 =  ` ! v1 v2 v3 (v4:real^3). let s = {v1,v2,v3,v4} in\r
1010   CARD s = 4 /\ coplanar s ==>\r
1011   conv0 s = aff_gt ( s DIFF {v1} ) {v1} INTER \r
1012   aff_gt ( s DIFF {v2} ) {v2} INTER \r
1013   aff_gt ( s DIFF {v3} ) {v3} INTER \r
1014   aff_gt ( s DIFF {v4} ) {v4} `;;\r
1015 (* le 83. p 52 *)\r
1016 let LEMMA83 =  ` !(e1:real^3) e2 e3 a b c a' b' c' t1 t2 t3.\r
1017   e1 = basis 1 /\\r
1018      e2 = basis 2 /\\r
1019      e3 = basis 3 /\\r
1020      &0 < a /\\r
1021      a <= b /\\r
1022      b <= c /\\r
1023      &0 < a' /\\r
1024      a' <= b' /\\r
1025      b' <= c' /\\r
1026      a <= a' /\\r
1027      b <= b' /\\r
1028      c <= c' /\\r
1029      (!x. x IN {t1, t2, t3} ==> &0 < x) /\\r
1030      t1 + t2 + t3 < &1 /\\r
1031      v =\r
1032      ((t1 + t2 + t3) * a) % e1 +\r
1033      ((t2 + t3) * sqrt (b pow 2 - a pow 2)) % e2 +\r
1034      (t3 * sqrt (c pow 2 - b pow 2)) % e3 /\\r
1035   v' = ((t1 + t2 + t3) * a') % e1 +\r
1036      ((t2 + t3) * sqrt (b' pow 2 - a' pow 2)) % e2 +\r
1037      (t3 * sqrt (c' pow 2 - b' pow 2)) % e3 ==>\r
1038   norm v <= norm v' `;;\r
1039 let TYUNJNA = LEMMA83 ;;\r
1040 \r
1041 (* le 84. p 53 *)\r
1042 let LEMMA84 =  ` ! x1 x2 x3 (x4:real^3).\r
1043   CARD {x1,x2,x3,x4} = 4 ==>\r
1044          let x12 = dist (x1,x2) pow 2 in\r
1045          let x13 = dist (x1,x3) pow 2 in\r
1046          let x14 = dist (x1,x4) pow 2 in\r
1047          let x23 = dist (x2,x3) pow 2 in\r
1048          let x24 = dist (x2,x4) pow 2 in\r
1049          let x34 = dist (x3,x4) pow 2 in\r
1050   &0 <= rho x12 x13 x14 x23 x24 x34  `;;\r
1051 let SHOGYBS = LEMMA84;;\r
1052 \r
1053 (* le 85. p53 *)\r
1054 \r
1055 let VBVYGGT =  ` ! v1 v2 v3 (v4:real^3).\r
1056   CARD {v1, v2, v3, v4} = 4 /\ ~coplanar {v1, v2, v3, v4}\r
1057          ==> (?!p. p = circumcenter {v1, v2, v3, v4} /\\r
1058                    (let x12 = dist (v1,v2) pow 2 in\r
1059                     let x13 = dist (v1,v3) pow 2 in\r
1060                     let x14 = dist (v1,v4) pow 2 in\r
1061                     let x23 = dist (v2,v3) pow 2 in\r
1062                     let x24 = dist (v2,v4) pow 2 in\r
1063                     let x34 = dist (v3,v4) pow 2 in\r
1064                     let chi11 = chi x12 x13 x14 x34 x24 x23 in\r
1065                     let chi22 = chi x12 x24 x23 x34 x13 x14 in\r
1066                     let chi33 = chi x34 x13 x23 x12 x24 x14 in\r
1067                     let chi44 = chi x34 x24 x14 x12 x13 x23 in\r
1068                     p =\r
1069                     &1 / (&2 * delta x12 x13 x14 x23 x24 x34) %\r
1070                     (chi11 % v1 + chi22 % v2 + chi33 % v3 + chi44 % v4))) `;;\r
1071 let LEMMA85 = VBVYGGT;;\r
1072 \r
1073 (* le 86. p 54 *)\r
1074 \r
1075 let GDRQXLG = ` ! v1 v2 v3 (v4:real^3).\r
1076   let s = {v1, v2, v3, v4} in\r
1077 let x12 = dist (v1,v2) pow 2 in\r
1078                     let x13 = dist (v1,v3) pow 2 in\r
1079                     let x14 = dist (v1,v4) pow 2 in\r
1080                     let x23 = dist (v2,v3) pow 2 in\r
1081                     let x24 = dist (v2,v4) pow 2 in\r
1082                     let x34 = dist (v3,v4) pow 2 in\r
1083 \r
1084      CARD s = 4 /\ ~coplanar s\r
1085      ==> radV s =\r
1086          sqrt (rho x12 x13 x14 x23 x24 x34) /\r
1087          (&2 * sqrt (delta x12 x13 x14 x23 x24 x34))` ;;\r
1088 let LEMMA86 = GDRQXLG;;\r
1089 \r
1090 (* le 87. p 54 *)\r
1091 \r
1092 let ZJEWPAP = ` ! v1 v2 v3 (v4:real^3).\r
1093   let s = {v1, v2, v3, v4} in CARD s = 4 /\ ~ coplanar s \r
1094   ==> radV {v1,v2,v3}  <= radV s  `;;\r
1095 \r
1096 \r
1097 (* LE 88, p 55 *)\r
1098 let LEMMA88 = ` ! v1 v2 v3 (v4:real^3).\r
1099          CARD {v1, v2, v3, v4} = 4\r
1100          ==> (let s = {v1, v2, v3, v4} in\r
1101               let x12 = dist (v1,v2) pow 2 in\r
1102               let x13 = dist (v1,v3) pow 2 in\r
1103               let x14 = dist (v1,v4) pow 2 in\r
1104               let x23 = dist (v2,v3) pow 2 in\r
1105               let x24 = dist (v2,v4) pow 2 in\r
1106               let x34 = dist (v3,v4) pow 2 in\r
1107               orientation s v1 (\t. t < &0) <=>\r
1108               chi x12 x13 x14 x23 x24 x34 < &0) `;;\r
1109 let VSMPQYO = LEMMA88;;\r
1110 \r
1111 (* LE 89. p 55 *)\r
1112 \r
1113 let LEMMA89 =  ` ! (v1:real^3) v2 v3 v4.\r
1114      let s = {v1, v2, v3, v4} in\r
1115      ~coplanar s\r
1116      ==> (circumcenter s IN conv0 s <=>\r
1117           orientation s v1 (\x. &0 < x) /\\r
1118           orientation s v2 (\x. &0 < x) /\\r
1119           orientation s v3 (\x. &0 < x) /\\r
1120           orientation s v4 (\x. &0 < x))`;;\r
1121 let PVLJZLA = LEMMA89;;\r
1122 (* le 90. p 55 *)\r
1123 \r
1124 let IAALCFJ =  ` ! (v1:real^3) v2 v3 v4.\r
1125      let s = {v1, v2, v3, v4} in\r
1126      CARD s = 4 /\\r
1127      packing s /\\r
1128      (!x y. {x, y} SUBSET s ==> d3 x y <= sqrt8) /\\r
1129      orientation s v1 (\x. x < &0)\r
1130      ==> (!x. x IN {v2, v3, v4} ==> orientation s x (\x. &0 <= x))`;;\r
1131 let LEMMA90 = IAALCFJ ;;\r
1132 \r
1133 (* le 91 . p 55 *)\r
1134 \r
1135 let YOEEQPC = ` ! (v1:real^3) v2 v3 v4.\r
1136      let s = {v1, v2, v3, v4} in\r
1137      let tt = #2.51 in\r
1138      CARD s = 4 /\\r
1139      packing s /\\r
1140      tt <= d3 v2 v4 /\\r
1141      d3 v2 v4 <= sqrt8 /\\r
1142      d3 v2 v3 <= tt /\\r
1143      d3 v3 v4 <= tt /\\r
1144      orientation s v1 (\x. x < &0)\r
1145      ==> (!x. x IN {v2, v3, v4} ==> d3 v1 x <= tt)`;;\r
1146 \r
1147 (* le 92. p 56 *)\r
1148 let YJTLEGD = ` ! (v1:real^3) v2 v3 v0.\r
1149   let s = {v1, v2, v3, v0} in\r
1150      let tt = #2.51 in\r
1151      CARD s = 4 /\\r
1152      packing s /\\r
1153      (!x y. {x, y} SUBSET {v1, v2, v3} ==> d3 x y <= tt) /\\r
1154      orientation s v0 (\x. x < &0)\r
1155      ==> (!x. x IN {v1, v2, v3} ==> &2 <= d3 v0 x /\ d3 v0 x <= tt)`;;\r
1156 \r
1157 let LEMMA92 = YJTLEGD;;\r
1158 \r
1159 (* le 93. p 56 *)\r
1160 let NJBVVWG = `! (v1:real^3) v2 v3 v4 x.\r
1161   let s = {v1, v2, v3, v4} in\r
1162      CARD s = 4 /\ packing s /\ x IN s /\ radV (s DELETE x) < sqrt (&2)\r
1163      ==> orientation s x (\x. &0 < x)`;;\r
1164 \r
1165 let LEMMA93 = NJBVVWG ;;\r
1166 \r
1167 \r
1168 \r
1169 (* le 95 . p 57 *)\r
1170 let GLQHFGH =  ` !v0 v1 v2 (v3:real^3).\r
1171   let s = {v0, v1, v2, v3} in\r
1172      CARD s = 4 /\\r
1173      packing s /\\r
1174      (!x y. {x, y} SUBSET {v1, v2, v3} ==> d3 x y <= sqrt8)\r
1175      ==> (~(conv {v1, v2, v3} INTER voronoi v0 s = {})\r
1176           ==> orientation s v0 (\x. x < &0)) /\\r
1177          (~(conv {v1, v2, v3} INTER voronoi_le v0 s = {})\r
1178           ==> orientation s v0 (\x. x <= &0))`;;\r
1179 let LEMMA95 = GLQHFGH;;\r
1180 (* le 97. p 58 *)\r
1181 let TCQPONA =  ` ! (v:real^3) v1 v2 v3.\r
1182   CARD {v, v1, v2, v3} = 4 /\\r
1183      packing {v, v1, v2, v3} /\\r
1184      (!a b. {a, b} SUBSET {v1, v2, v3} ==> d3 a b <= #2.51) /\\r
1185      ~(conv {v1, v2, v3} INTER voronoi v {v1, v2, v3} = {})\r
1186      ==> (!x. x IN {v1, v2, v3} ==> &2 <= d3 x v /\ d3 x v < #2.51)`;;\r
1187 let LEMMA97 = TCQPONA ;;\r
1188 \r
1189 (* le 98. p 59 *)\r
1190 let CEWWWDQ =  ` ! (v:real^3) v1 v2 v3.\r
1191      let s = {v, v1, v2, v3} in\r
1192      let dd = #2.51 in\r
1193      CARD s = 4 /\\r
1194      packing s /\\r
1195      d3 v1 v3 <= dd /\\r
1196      d3 v2 v3 <= dd /\\r
1197      d3 v1 v3 <= sqrt8 /\\r
1198      ~(conv (s DELETE v) INTER voronoi v s = {})\r
1199      ==> (!x. x IN {v1, v2, v3} ==> &2 <= d3 v x /\ d3 v x <= dd)`;;\r
1200 let LEMMA98 = CEWWWDQ;;\r
1201 \r
1202 (* le 99. *)\r
1203 let CKLAKTB =  ` !(w:real^3) v0 v1 v2 x.\r
1204      (!x y. {x, y} SUBSET {v0, v1, v2} ==> d3 x y < sqrt (&8)) /\\r
1205      CARD {w, v0, v1, v2} = 4 /\ packing {w, v0, v1, v2} /\\r
1206      ~(conv {x, w} INTER cone v0 {v1, v2} = {}) /\\r
1207      d3 x v0 < d3 x v1 /\\r
1208      d3 x v0 < d3 x v2 /\\r
1209      d3 x w < d3 x v0\r
1210      ==> ~(conv {x, w} INTER conv {v0, v1, v2} = {})`;;\r
1211 let LEMMA99 = CKLAKTB ;;\r
1212 \r
1213 (* le 100. p 60 *)\r
1214 \r
1215 let UMMNOJN = ` ! (x:real^3) w v0 v1 v2.\r
1216   CARD {w, v0, v1, v2} = 4 /\\r
1217      packing {w, v0, v1, v2} /\\r
1218      conv {x, w} INTER cone v0 {v1, v2} = {} /\\r
1219      d3 x v0 < d3 x v1 /\\r
1220      d3 x v0 < d3 x v2 /\\r
1221      d3 x w < d3 x v0 /\\r
1222      (!x y. {x, y} SUBSET {v0, v1, v2} ==> d3 x y < sqrt (&8)) /\\r
1223      ((!x y. {x, y} SUBSET {v0, v1, v2} ==> d3 x y <= #2.51) \/\r
1224       (?x y.\r
1225            {x, y} SUBSET {v0, v1, v2} /\\r
1226            ~(d3 x y <= #2.51) /\\r
1227            (!xx yy.\r
1228                 {xx, yy} SUBSET {v0, v1, v2} /\ ~(d3 xx yy <= #2.51)\r
1229                 ==> {xx, yy} = {x, y}))) ==>\r
1230   (! x. x IN {v0,v1,v2} ==> d3 w x <= #2.51 )/\\r
1231   ~ ( conv {x,w} INTER conv {v0,v1,v2} = {} ) `;;\r
1232 let LEMMA100 = UMMNOJN;;\r
1233 (* le 101, not presented in the book *)\r
1234 \r
1235 (* le 102. p 60 *)\r
1236 let XBNRPGQ = ` ! v0 v1 w0 (w1:real^3) c0 c1.\r
1237   let s = {v0, v1, w0, w1} in\r
1238      let F' = {v0, v1, w1} in\r
1239      CARD {v0, v1, w0, w1} = 4 /\\r
1240      packing {v0, v1, w0, w1} /\\r
1241      sqrt (&2) <= radV s /\\r
1242      ~coplanar s /\\r
1243      radV {v0, v1, w0} < sqrt (&2) /\\r
1244      c0 = circumcenter {v0, v1, w0} /\\r
1245      d3 v0 c1 = sqrt (&2) /\\r
1246      d3 v1 c1 = sqrt (&2) /\\r
1247      d3 w0 c1 = sqrt (&2) /\\r
1248      c1 IN aff_gt {v0, v1, w0} {w1} /\\r
1249      radV F' < sqrt (&2) /\\r
1250      (?u v w.\r
1251           F' = {u, v, w} /\\r
1252           d3 u v <= #2.51 /\\r
1253           d3 v w <= #2.51 /\\r
1254           d3 u w <= sqrt (&8) /\\r
1255           (?xa. xa IN F' /\ d3 xa w0 > #2.51))\r
1256      ==> conv {c0, c1} INTER aff {v0, v1, w0} = {}` ;;\r
1257 let LEMMA102 = XBNRPGQ;;\r
1258 \r
1259 (* le 103. p 61 *)\r
1260 \r
1261 let MITDERY = ` ! v0 v w (w':real^3) c.\r
1262   let tt = #2.51 in\r
1263      let s = {v0, v, w, w'} in\r
1264      CARD s = 4 /\\r
1265      tt <= d3 v v0 /\\r
1266      d3 v v0 <= sqrt8 /\\r
1267      tt < d3 w w' /\\r
1268      d3 w w' <= sqrt8 /\\r
1269      (!x y.\r
1270           {x, y} SUBSET s /\ ~({x, y} = {v, v0} \/ {x, y} = {w, w'})\r
1271           ==> d3 x y <= tt) /\\r
1272      c <= radV s\r
1273      ==> rogers v0 w v w' c SUBSET conv s`;;\r
1274 let LEMMA103 = MITDERY;;\r
1275 \r
1276 (* le 104. p 61 *)\r
1277 let BAJSVHC =  ` ! v1 v2 v3 v4 (v5:real^3).\r
1278    CARD {v1, v2, v3, v4, v5} = 5 /\\r
1279      ~coplanar {v1, v2, v3, v4} /\\r
1280      v5 IN aff_ge {v1, v3} {v2, v4} /\\r
1281      ~(v5 IN aff {v1, v3})\r
1282      ==> aff_ge {v1, v3} {v2, v4} =\r
1283          aff_ge {v1, v3} {v2, v5} UNION aff_ge {v1, v3} {v4, v5} /\\r
1284          aff_gt {v1, v3} {v2, v5} INTER aff_gt {v1, v3} {v4, v5} = {}`;;\r
1285 let LEMMA104 = BAJSVHC;;\r
1286 \r
1287 (* le 105. p 62 *)\r
1288 \r
1289 let TBMYVLM = ` !v0 v1 v2 v3 (v4:real^3) .\r
1290      let s = {v0, v1, v2, v3, v4} in\r
1291      CARD s = 5 /\\r
1292      (!x. x IN {v1, v2, v3} ==> ~coplanar (s DELETE x)) /\\r
1293      v4 IN cone v0 {v1, v2, v3}\r
1294      ==> (!x. x IN\r
1295               aff_ge {v0, v4} {v1, v2} UNION\r
1296               aff_ge {v0, v4} {v1, v3} UNION\r
1297               aff_ge {v0, v4} {v2, v3}) /\\r
1298          (!x y.\r
1299               ~(x = y) /\ {x, y} SUBSET {v1, v2, v3}\r
1300               ==> aff_gt {v0, v4} ({v1, v2, v3} DELETE x) INTER\r
1301                   aff_gt {v0, v4} ({v1, v2, v3} DELETE y) =\r
1302                   {})`;;\r
1303 let LEMMA105 = TBMYVLM;;\r
1304 (* le 106. p 63 *)\r
1305 let TQLZOUG = ` !v0 (v1:real^3) v2 v3 R R0 c3 s.\r
1306   s = {v0, v1, v2, v3} /\\r
1307      p = circumcenter s /\\r
1308      c3 = circumcenter {v0, v1, v2} /\\r
1309      R = rogers v0 v1 v2 v3 (radV s) /\\r
1310      R0 = rogers0 v0 v1 v2 v3 (radV s) /\\r
1311      CARD s = 4 /\\r
1312      packing s /\\r
1313      (!x. x IN {v1, v2, v3} ==> orientation s x (\x. &0 < x)) /\\r
1314      d3 v1 v2 < sqrt (&8) /\\r
1315      d3 v2 v3 < sqrt (&8) /\\r
1316      d3 v3 v1 < sqrt (&8)\r
1317      ==> voronoi v0 s INTER\r
1318          aff_ge {v0, p} {v1, c3} INTER\r
1319          cone v0 {v1, v2, v3} SUBSET\r
1320          R /\\r
1321          R0 =\r
1322          voronoi v0 s INTER\r
1323          aff_gt {v0, p} {v1, c3} INTER\r
1324          cone0 v0 {v1, v2, v3}`;;\r
1325 let LEMMA106 = TQLZOUG;;\r
1326 \r
1327 (* le 107. p 64 *)\r
1328 \r
1329 let UREVUCX = ` !v0 v1 v2 (v3:real^3).\r
1330        let s = {v0, v1, v2, v3} in\r
1331      CARD s = 4 /\\r
1332      packing s /\\r
1333      (!x. x IN {v1, v2, v3} ==> orientation s x (\x. &0 < x)) /\\r
1334      (!x y. {x, y} SUBSET {v1, v2, v3} ==> d3 x y < sqrt (&8))\r
1335      ==> UNIONS {rogers0 v0 u v w (radV s) | {u, v, w} = {v1, v2, v3}} SUBSET\r
1336          cone v0 {v1, v2, v3} INTER voronoi v0 s /\\r
1337          cone v0 {v1, v2, v3} INTER voronoi v0 s SUBSET\r
1338          UNIONS {rogers v0 u v w (radV s) | {u, v, w} = {v1, v2, v3}}`;;\r
1339 let LEMMA107 = UREVUCX;;\r
1340 \r
1341 \r
1342 (* le 108. p 65 *)\r
1343 let RKWVONN = ` !v0 v1 v2 (v3:real^3).\r
1344       let s = {v0, v1, v2, v3} in\r
1345      CARD s = 4 /\\r
1346      packing s /\\r
1347      (!x. x IN {v1, v2, v3} ==> orientation s x (\x. &0 < x)) /\\r
1348      (!x y. {x, y} SUBSET {v1, v2, v3} ==> d3 x y < sqrt (&8))\r
1349      ==> voronoi_le v0 s INTER aff_le {v1, v2, v3} {v0} SUBSET\r
1350          cone v0 {v1, v2, v3}`;;\r
1351 let LEMMA108 = RKWVONN;;\r
1352 \r
1353 \r
1354 \r
1355 let phi_fun = new_definition ` phi_fun  S v u = \r
1356   { x| ? x'. x' IN aff_gt {v} {x} /\ dist (x',u ) = dist (x',v) /\\r
1357   ( ! w. w IN S ==> dist (x',v) <= dist (x',w) ) }`;;\r
1358 \r
1359 (* le 109. p 65 *)\r
1360 let EMLLARA = ` !u (v:real^3) w.\r
1361      (collinear {u, v, w} ==> bis u v INTER bis v w = {}) /\\r
1362   ( ~collinear {u, v, w} ==> line ( bis u v INTER bis v w )) `;;\r
1363 \r
1364 let LEMMA109 = EMLLARA;;\r
1365 \r
1366 (* le 110. p 66 *)\r
1367 let DKCSJPZ = `! u v (w:real^3) x p.\r
1368   let s = {u, v, w} in\r
1369      x IN phi_fun s v u INTER phi_fun s v w /\\r
1370      ~(u = w) /\\r
1371      plane p /\\r
1372      v IN p /\\r
1373      bis u v INTER bis v w SUBSET p\r
1374      ==> x IN p`;;\r
1375 \r
1376 let LEMMA110 = DKCSJPZ;;\r
1377 \r
1378 \r
1379 let phi_fun' = new_definition ` phi_fun' S v u w = \r
1380   {x | FINITE S /\\r
1381               (?x''. x IN aff_gt {v} {x'', u} /\\r
1382                      dist (x'',u) = dist (x'',v) /\\r
1383                      dist (x'',u) = dist (x'',w) /\\r
1384                      (!w'. w' IN S ==> dist (x'',v) <= dist (x'',w')))} `;;\r
1385 \r
1386 (* le 111. p 66 *)\r
1387 let QXSXGMC = ` ! (u:real^3) v S. convex ( phi_fun S u v ) `;;\r
1388 let LEMMA111 = QXSXGMC;;\r
1389 \r
1390 (* le 112 . p 67 *)\r
1391 \r
1392 let IXOUEVV = ` ! u v (w:real^3) S. \r
1393   FINITE ( S UNION { u, v, w} ) /\ \r
1394   packing ( S UNION { u, v, w} ) /\\r
1395   dist (u,v) < sqrt (&8) \r
1396   ==> phi_fun' S v u w SUBSET phi_fun S v u `;;\r
1397 \r
1398 let LEMMA112 = IXOUEVV;;\r
1399 \r
1400 (* le 113. p 67 *)\r
1401 let KMTAMFH = ` ! v0 v1 v2 (v3:real^3).\r
1402   let S = {v0, v1, v2, v3} in\r
1403      CARD S = 4 /\\r
1404      ~coplanar S /\\r
1405      d3 v1 v2 < sqrt (&8) /\\r
1406      d3 v2 v3 < sqrt (&8) /\\r
1407      ~(cone v2 {v1, v3} INTER phi_fun {v0, v1, v3} v2 v0 = {})\r
1408      ==> orientation S v0 (\x. x <= &0)`;;\r
1409 let LEMMA113 = KMTAMFH;;\r
1410 \r
1411 (* le 114. p 68 *)\r
1412 let JHOQMMR = ` ! v0 v1 u1 (u2:real^3).\r
1413   let s = {v0, v1, u1, u2} in\r
1414      let y = d3 v1 v0 in\r
1415      let bb = eta_y (&2) #2.51 y in\r
1416      CARD s = 4 /\\r
1417      packing s /\\r
1418      d3 v0 v1 < sqrt (&8) /\\r
1419      d3 v0 u1 < sqrt (&8) /\\r
1420      d3 v0 u2 < sqrt (&8) /\\r
1421      d3 u1 u2 < sqrt (&8) /\\r
1422      #2.51 < d3 v1 v0 /\\r
1423      ((?a b.\r
1424            {a, b} SUBSET {v0, u1, u2} /\\r
1425            #2.51 < d3 a b /\\r
1426            (!aa bb.\r
1427                 {aa, bb} SUBSET {v0, u1, u2} /\ ~({aa, bb} = {a, b})\r
1428                 ==> d3 aa bb <= #2.51)) \/\r
1429       (!aa bb.\r
1430            {aa, bb} SUBSET {v0, u1, u2} /\ ~({aa, bb} = {a, b})\r
1431            ==> d3 aa bb <= #2.51)) /\\r
1432      x IN cone v0 {u1, u2} INTER rcone_gt v0 v1 (y / ( &2 * bb ))\r
1433      ==> (!x. x IN {d3 v1 u1, d3 v1 u2, d3 v0 u1, d3 v0 u2} ==> x <= #2.51) /\\r
1434          radV s < bb`;;\r
1435 let LEMMA114 = JHOQMMR;;\r
1436 \r
1437 (* le 115. pa 68 *)\r
1438 let YFTQMLF = ` ! v0 v1 u1 (u2:real^3).\r
1439   let s = {v0, v1, u1, u2} in\r
1440      let y = d3 v1 v0 in\r
1441      let bb = eta_y (&2) #2.51 y in\r
1442      CARD s = 4 /\\r
1443      packing s /\\r
1444      d3 v0 v1 < sqrt (&8) /\\r
1445      d3 v0 u1 < sqrt (&8) /\\r
1446      d3 v0 u2 < sqrt (&8) /\\r
1447      d3 u1 u2 < sqrt (&8) /\\r
1448      #2.51 < d3 v1 v0 /\\r
1449      ((?a b.\r
1450            {a, b} SUBSET {v0, u1, u2} /\\r
1451            #2.51 < d3 a b /\\r
1452            (!aa bb.\r
1453                 {aa, bb} SUBSET {v0, u1, u2} /\ ~({aa, bb} = {a, b})\r
1454                 ==> d3 aa bb <= #2.51)) \/\r
1455       (!aa bb.\r
1456            {aa, bb} SUBSET {v0, u1, u2} /\ ~({aa, bb} = {a, b})\r
1457            ==> d3 aa bb <= #2.51)) /\\r
1458      ~(w' IN affine hull {v0, v1, u1}) /\\r
1459      ~(cone v0 {u1, u2} INTER rogers v0 u1 v1 w' bb = {})\r
1460      ==> (!x. x IN {d3 v1 u1, d3 v1 u2, d3 v0 u1, d3 v0 u2} ==> x <= #2.51) /\\r
1461          radV s < bb`;;\r
1462 let LEMMA115 = YFTQMLF ;;\r
1463 \r
1464 (* LE 116 . p 69 *)\r
1465 let GQMZTHN = ` !(v0:real^3) v1 w u1 u2 b p y.\r
1466      let s = {v0, v1, w, u1, u2} in\r
1467      CARD s = 5 /\\r
1468      packing s /\\r
1469      d3 v0 u1 < sqrt (&8) /\\r
1470      d3 v0 u2 < sqrt (&8) /\\r
1471      d3 u1 u2 < sqrt (&8) /\\r
1472      d3 w v0 <= #2.51 /\\r
1473      #2.51 < d3 v0 v1 /\\r
1474      d3 v0 v1 < sqrt (&8) /\\r
1475      d3 v1 w <= #2.51 /\\r
1476      ((?a b.\r
1477            {a, b} SUBSET {v0, u1, u2} /\\r
1478            #2.51 < d3 a b /\\r
1479            (!aa bb.\r
1480                 {aa, bb} SUBSET {v0, u1, u2} /\ ~({aa, bb} = {a, b})\r
1481                 ==> d3 aa bb <= #2.51)) \/\r
1482       (!a b. {a, b} SUBSET {v0, u1, u2} ==> d3 a b <= #2.51)) /\\r
1483      y = d3 v0 v1 /\\r
1484      b = eta_y (&2) #2.51 y /\\r
1485      ~(phi_fun {w, u1, u2} v0 w INTER\r
1486        cone v0 {u1, u2} INTER\r
1487        rogers0 v0 w v1 p b =\r
1488        {}) /\\r
1489      ~(p IN affine hull {v0, w, v1})\r
1490      ==> d3 w u1 <= #2.51 /\\r
1491          d3 w u2 <= #2.51 /\\r
1492          ((?u. u IN {u1, u2} /\\r
1493                ~(rogers0 v0 w v1 p b INTER cone v0 {w, u} = {})) \/\r
1494           d3 u1 u2 < sqrt (&8) /\\r
1495           v1 IN cone0 v0 {w, u1, u2} /\\r
1496           d3 v1 u1 <= #2.51 /\\r
1497           d3 w u2 <= #2.51 \/\r
1498           #2.51 < d3 u1 u2 /\\r
1499           d3 u1 u2 < sqrt (&8) /\\r
1500           w IN aff_ge {v0, v1} {u1, u2})`;;\r
1501 let LEMMA116 = GQMZTHN;;\r
1502 \r
1503 (* definition in page 70 *)\r
1504 let split = new_definition` split v0 v1 w u1 w' p =\r
1505   ( radV {v0, v1, w, u1} < eta_y (d3 w v0) (&2) #2.51 /\\r
1506          u1 IN aff_ge {v0, v1, w} {p}\r
1507          ==> w' IN aff_gt {v0, v1} {w, u1} /\\r
1508              radV {v0, v1, w, w'} >= eta_y (d3 v0 v1) (&2) #2.51 /\\r
1509              d3 w' v1 <= #2.51 /\\r
1510              d3 w' v0 <= #2.51 /\\r
1511              #2.77 <= d3 w' w ) `;;\r
1512 \r
1513 \r
1514 (* le 117. p 68 *)\r
1515 let KWOHVUP = `! (v0:real^3) v1 w u1 u2 w' b p y.\r
1516   let s = {v0, v1, w, u1, u2, w'} in\r
1517      let ca = sqrt (&8) in\r
1518      let ha = #2.51 in\r
1519      CARD s = 6 /\\r
1520      packing s /\\r
1521      ~(p IN affine hull {v0, w, v1}) /\\r
1522      split v0 v1 w u1 w' p /\\r
1523      d3 v0 u1 < ca /\\r
1524      d3 v0 u2 < ca /\\r
1525      d3 u1 u2 < ca /\\r
1526      d3 v0 v1 < ca /\\r
1527      ha < d3 v0 v1 /\\r
1528      d3 w v0 <= ha /\\r
1529      d3 w v1 <= ha /\\r
1530      ((?a b.\r
1531            {a, b} SUBSET {v0, u1, u2} /\\r
1532            #2.51 < d3 a b /\\r
1533            (!aa bb.\r
1534                 {aa, bb} SUBSET {v0, u1, u2} /\ ~({aa, bb} = {a, b})\r
1535                 ==> d3 aa bb <= #2.51)) \/\r
1536       (!a b. {a, b} SUBSET {v0, u1, u2} ==> d3 a b <= #2.51)) /\\r
1537      y = d3 v1 v0 /\\r
1538      b = eta_y (&2) ha y /\\r
1539      ~(phi_fun {v1, w, u1, u2} v0 u1 INTER\r
1540        cone v0 {u1, u2} INTER\r
1541        rogers0 v0 w v1 p b =\r
1542        {})\r
1543      ==> d3 v0 v1 <= #2.51 /\\r
1544          d3 v1 u1 <= #2.51 /\\r
1545          d3 v1 w <= #2.51 /\\r
1546          u2 IN aff_gt {v0, u1} {v1, w} \/\r
1547          d3 v0 u1 <= ha /\\r
1548          d3 v1 u1 <= ha /\\r
1549          d3 u1 w < ha /\\r
1550          rogers0 v0 w v1 p b SUBSET aff_ge {v0, v1, w} {u1} \/\r
1551          (!v u. v IN {v0, v1} /\ u IN {u1, u2} ==> d3 u v <= #2.51) /\\r
1552          d3 w' v0 <= ha /\\r
1553          d3 w' v1 <= ha /\\r
1554          w' IN aff_gt {v0, v1} {u1, u2}`;;\r
1555 let LEMMA117 = KWOHVUP;;\r
1556 \r
1557 \r
1558 (* le 118. p 72 *)\r
1559 let UJCUNAS = ` !v0 v1 w u1 u2 w' p F_SET R b y.\r
1560      let s = {v0, v1, w, u1, u2, w'} in\r
1561      let zzz = #2.51 in\r
1562      let set_d = {v0, u1, u2} in\r
1563      CARD s = 6 /\\r
1564      packing s /\\r
1565      ~(p IN affine hull {v0, w, v1}) /\\r
1566      split v0 v1 w u1 w' p /\\r
1567      split v0 v1 w u2 w' p /\\r
1568      d3 v0 u1 < sqrt8 /\\r
1569      d3 v0 u2 < sqrt8 /\\r
1570      d3 u1 u2 < sqrt8 /\\r
1571      d3 w v0 <= zzz /\\r
1572      zzz < d3 v0 v1 /\\r
1573      d3 v0 v1 < sqrt8 /\\r
1574      d3 v1 w <= zzz /\\r
1575      ((?a b.\r
1576            {a, b} SUBSET set_d /\\r
1577            zzz < d3 a b /\\r
1578            (!aa bb.\r
1579                 {aa, bb} SUBSET set_d /\ ~({aa, bb} = {a, b})\r
1580                 ==> d3 aa bb <= zzz)) \/\r
1581       (!a b. {a, b} SUBSET set_d ==> d3 a b <= zzz)) /\\r
1582      y = d3 v1 v0 /\\r
1583      b = eta_y (&2) zzz y /\\r
1584      F_SET = cone v0 {u1, u2} /\\r
1585      R = rogers0 v0 w v1 p b\r
1586      ==> d3 w u1 <= zzz /\\r
1587          d3 w u2 <= zzz /\\r
1588          (!u. u = u1 \/ u = u2 ==> ~(R INTER cone v0 {w, u} = {})) \/\r
1589          d3 w u1 <= zzz /\\r
1590          d3 w u2 <= zzz /\\r
1591          d3 u1 u2 < sqrt8 /\\r
1592          v1 IN cone0 v0 {w, u1, u2} /\\r
1593          d3 v1 u1 <= zzz /\\r
1594          d3 v1 u2 <= zzz \/\r
1595          d3 w u1 <= zzz /\\r
1596          d3 w u2 <= zzz /\\r
1597          zzz < d3 u1 u2 /\\r
1598          d3 u1 u2 < sqrt8 /\\r
1599          w IN aff_ge {v0, v1} {u1, u2} \/\r
1600          (?u u'.\r
1601               {u, u'} = {u1, u2} /\\r
1602               d3 v0 u <= zzz /\\r
1603               d3 v1 u <= zzz /\\r
1604               d3 u w <= zzz /\\r
1605               u' IN aff_gt {v0, u} {v1, w}) \/\r
1606          (?u. u IN {u1, u2} /\\r
1607               d3 v0 u <= zzz /\\r
1608               d3 v1 u <= zzz /\\r
1609               d3 u w <= zzz /\\r
1610               R SUBSET aff_ge {v0, v1, w} {u}) \/\r
1611          (!v u''. v IN {v0, v1} /\ u'' IN {u1, u2} ==> d3 v u'' <= zzz) /\\r
1612          d3 w' v0 <= zzz /\\r
1613          d3 w' v1 <= zzz /\\r
1614          w' IN aff_gt {v0, v1} {u1, u2}`;;\r
1615 let LEMMA118 = UJCUNAS;;\r
1616 (* le 119 . p 73 *)\r
1617 \r
1618 let DVLHHMF = ` ! R' R0 b v0 v w w' u.\r
1619      let s = {v0, v, w, w', u} in\r
1620      let zz = #2.51 in\r
1621      CARD s = 5 /\\r
1622      packing s /\\r
1623      zz < d3 v0 v /\\r
1624      d3 v0 v < sqrt8 /\\r
1625      zz < d3 w w' /\\r
1626      (!v' w''. v' IN {v0, v} /\ w'' IN {w, w', u} ==> d3 v' w'' <= zz) /\\r
1627      b = eta_y (&2) zz (d3 v v0) /\\r
1628      b <= radV {v0, v, w, w'} /\\r
1629      ~(conv {w, u} INTER aff_ge {v0, v} {w'} = {}) /\\r
1630      R0 = rogers0 v0 w v u b /\\r
1631      R' = R0 INTER voronoi v0 {w, u} INTER phi_fun {v0, w, u} v0 u /\\r
1632      ~(R' = {})\r
1633      ==> (!x. x IN R' ==> ~(conv {x, u} INTER conv {v0, v, w'} = {})) /\\r
1634          d3 u w' <= zz`;;\r
1635 \r
1636 let LEMMA119 = DVLHHMF;;\r
1637 \r
1638 (* le 120 . 74 *)\r
1639 let UIXOFDB = ` !v0 v1 v1' w1 w2 b b'.\r
1640      let s = {v0, v1, v1', w1, w2} in\r
1641      let zz = #2.51 in\r
1642      CARD s = 5 /\\r
1643      packing s /\\r
1644      zz <= d3 v0 v1 /\\r
1645      d3 v0 v1 < sqrt8 /\\r
1646      zz <= d3 v0 v1' /\\r
1647      d3 v0 v1' < sqrt8 /\\r
1648      (!v w. v IN {v0, v1} /\ w IN {w1, w2} ==> d3 v w <= zz) /\\r
1649      ~coplanar {v0, v1, w1, w2} /\\r
1650      b' = d3 v0 v1' / (&2 * eta_y (d3 v0 v1') (&2) zz) /\\r
1651      b = d3 v0 v1 / (&2 * eta_y (d3 v0 v1) (&2) zz)\r
1652      ==> rogers0 v0 w1 v1 w2 b INTER rcone_ge v0 v1' b' = {}`;;\r
1653 let LEMMA120 = UIXOFDB;;\r
1654 \r
1655 (* le 121. p74 *)\r
1656 let MJNUTQH = ` !v0 v1 v2 w1 w2 p1 p2.\r
1657      let s = {v0, v1, v2, w1, w2} in\r
1658      let zz = #2.51 in\r
1659      CARD s = 5 /\\r
1660      packing s /\\r
1661      zz <= d3 v0 v1 /\\r
1662      d3 v0 v1 < sqrt8 /\\r
1663      zz <= d3 v0 v2 /\\r
1664      d3 v0 v2 < sqrt8 /\\r
1665      (!w. w IN {w1, w2} ==> d3 v0 w <= zz) /\\r
1666      d3 v1 w1 <= zz /\\r
1667      d3 v2 w2 <= zz /\\r
1668      ~coplanar {v0, v1, w1, p1} /\\r
1669      ~coplanar {v0, v2, w2, p2} /\\r
1670      b1 = eta_y (d3 v0 v1) (&2) zz /\\r
1671      b2 = eta_y (d3 v0 v2) (&2) zz /\\r
1672      ~(rogers v0 w1 v1 p1 b1 INTER rogers v0 w2 v2 p2 b2 = {})\r
1673      ==> d3 v1 w2 <= zz /\\r
1674          (d3 w1 w2 <= zz /\\r
1675           (~(rogers0 v0 w2 v2 p2 b2 INTER aff_ge {v0} {v1, w1} = {}) \/\r
1676            aff_ge {v0, v1, w1} {w2} = aff_ge {v0, v1, w1} {p1}) \/\r
1677           zz < d3 w1 w2 /\\r
1678           ~(phi_fun {v0, v1, w1, w2} v0 w2 INTER rogers v0 w1 v1 p1 b1 = {}) /\\r
1679           radV {v0, v1, w1, w2} < b1 /\\r
1680           aff_ge {v0, v1, w1} {w2} = aff_ge {v0, v1, w1} {p1}) \/\r
1681          d3 v2 w1 <= zz /\\r
1682          (d3 w1 w2 <= zz /\\r
1683           (~(rogers0 v0 w1 v1 p1 b1 INTER aff_ge {v0} {v2, w2} = {}) \/\r
1684            aff_ge {v0, v2, w2} {w1} = aff_ge {v0, v2, w2} {p2}) \/\r
1685           zz < d3 w1 w2 /\\r
1686           ~(phi_fun {v0, v1, w1, w2} v0 w1 INTER rogers v0 w2 v2 p2 b2 = {}) /\\r
1687           radV {v0, v2, w1, w2} < b2 /\\r
1688           aff_ge {v0, v2, w2} {w2} = aff_ge {v0, v2, w2} {p2})`;;\r
1689 \r
1690 let LEMMA121 = MJNUTQH;;\r
1691 \r
1692 (* le 122 . 75 *)\r
1693 \r
1694 let MPJEZGP = ` !t0 t1 t2 t3 t4 v0 v1 v2 v3 v4.\r
1695      CARD {v0, v1, v2, v3, v4} = 5 /\\r
1696      t0 % v0 + t1 % v1 + t2 % v2 + t3 % v3 + t4 % v4 = vec 0 /\\r
1697      t4 < &0 /\\r
1698      t0 + t1 + t2 + t3 + t4 = &0\r
1699      ==> ((!t. t IN {t1, t2, t3} ==> &0 <= t) <=> v4 IN cone v0 {v1, v2, v3}) /\\r
1700          (&0 <= t1 /\ &0 <= t3 /\ t2 <= &0 <=>\r
1701           ~(cone v0 {v2, v4} INTER cone v0 {v1, v3} = {})) /\\r
1702          (&0 <= t1 /\ &0 <= t2 /\ t3 <= &0 <=>\r
1703           ~(cone v0 {v3, v4} INTER cone v0 {v1, v2} = {})) /\\r
1704          (&0 <= t1 /\ &0 <= t2 /\ t3 <= &0 <=>\r
1705           ~(cone v0 {v1, v4} INTER cone v0 {v2, v3} = {})) /\\r
1706          (&0 <= t1 /\ t2 <= &0 /\ t3 <= &0 <=> v1 IN cone v0 {v2, v3, v4}) /\\r
1707          (&0 <= t2 /\ t1 <= &0 /\ t3 <= &0 <=> v2 IN cone v0 {v1, v3, v4}) /\\r
1708          (&0 <= t3 /\ t1 <= &0 /\ t2 <= &0 <=> v3 IN cone v0 {v2, v1, v4}) /\\r
1709          (&0 <= t0 /\ t1 <= &0 /\ t2 <= &0 /\ t3 <= &0 <=>\r
1710           v0 IN conv {v1, v2, v3, v4}) /\\r
1711          ~(t0 < &0 /\ (!t. t IN {t1, t2, t3} ==> t <= &0))`;;\r
1712 \r
1713 let LEMMA122 = MPJEZGP;;\r
1714 \r
1715 \r
1716 (* le 123 . p 76 *)\r
1717 let GFVQUPP = ` !x1 x2 x3 x4.\r
1718      let x12 = dist (x1,x2) pow 2 in\r
1719      let x13 = dist (x1,x3) pow 2 in\r
1720      let x14 = dist (x1,x4) pow 2 in\r
1721      let x23 = dist (x2,x3) pow 2 in\r
1722      let x24 = dist (x2,x4) pow 2 in\r
1723      let x34 = dist (x3,x4) pow 2 in\r
1724      (!x. x IN {x12, x13, x14, x34, x24} ==> x <= #2.517 pow 2) /\\r
1725      #2.65 pow 2 <= x23\r
1726      ==> delta_x23 x12 x13 x14 x34 x24 x23 > &0`;;\r
1727 \r
1728 let LEMMA123 = GFVQUPP;;\r
1729 \r
1730 \r
1731 (* le 124 . p 76 *)\r
1732 let TFKALQL = ` !v1 v2 v3 v4.\r
1733      let s = {v1, v2, v3, v4} in\r
1734      let x12 = dist (v1,v2) pow 2 in\r
1735      let x13 = dist (v1,v3) pow 2 in\r
1736      let x14 = dist (v1,v4) pow 2 in\r
1737      let x23 = dist (v2,v3) pow 2 in\r
1738      let x24 = dist (v2,v4) pow 2 in\r
1739      let x34 = dist (v3,v4) pow 2 in\r
1740      CARD s = 4 /\\r
1741      packing s /\\r
1742      x12 <= #2.3 pow 2 /\\r
1743      (!x. x IN {x13, x14, x34, x24} ==> x <= #2.517 pow 2) /\\r
1744      #2.51 pow 2 <= x23\r
1745      ==> delta_x23 x12 x13 x24 x34 x24 x23 > &0`;;\r
1746 \r
1747 let LEMMA124 = TFKALQL;;\r
1748 \r
1749 (* le 125 . p 77 *)\r
1750 \r
1751 let AAGNQFL = `!v0 v1 v2 v3 v4.\r
1752      let s = {v0, v1, v2, v3, v4} in\r
1753      CARD s = 5 /\\r
1754      packing s /\\r
1755      (!u v.\r
1756           {u, v} SUBSET s /\ ~({u, v} = {v1, v3} \/ {u, v} = {v2, v4})\r
1757           ==> d3 u v <= #2.51) /\\r
1758      v1 IN cone v0 {v2, v3, v4}\r
1759      ==> d3 v1 v3 < #2.65`;;\r
1760 \r
1761 let LEMMA125 = AAGNQFL;;\r
1762 \r
1763 (* le 126 . p 77 *)\r
1764 let QOKQFRE = ` !v0 v1 v2 v3 v4.\r
1765      let s = {v0, v1, v2, v3, v4} in\r
1766      CARD s = 5 /\\r
1767      packing s /\\r
1768      (!u v.\r
1769           {u, v} SUBSET s /\ ~({u, v} = {v1, v3} \/ {u, v} = {v2, v4})\r
1770           ==> d3 u v <= #2.51) /\\r
1771      d3 v0 v1 <= #2.3 /\\r
1772      v1 IN cone v0 {v2, v3, v4}\r
1773      ==> d3 v1 v3 < #2.51`;;\r
1774 \r
1775 let LEMMA126 = QOKQFRE ;;\r
1776 \r
1777 let quadp = new_definition ` quadp v0 v1 v2 v3 v4 =\r
1778   ~ (cone0 v0 {v1,v3} INTER cone0 v0 {v2,v4} = {} ) `;;\r
1779 \r
1780 let quadc0 = new_definition ` quadc0 v0 v1 v2 v3 v4 =\r
1781          (@h. quadp v0 v1 v2 v3 v4 /\\r
1782               h =\r
1783               cone0 v0 {v1, v2, v3} INTER\r
1784               cone0 v0 {v1, v3} INTER\r
1785               cone0 v0 {v1, v3, v4}) `;;\r
1786 (* le 127. p 78 *)\r
1787 let DFLUMBW = `!v0 v1 v2 v3 v4.\r
1788      CARD {v0, v1, v2, v3, v4} = 5 /\ quadp v0 v1 v2 v3 v4\r
1789      ==> quadc0 v0 v1 v2 v3 v4 = quadc0 v0 v2 v3 v4 v1`;;\r
1790 \r
1791 let LEMMA127 = DFLUMBW;;\r
1792 \r
1793 (* le 128 . p 78 *)\r
1794 \r
1795 let HTYDGWI = ` !v0 v1 v2 v3 v4.\r
1796      CARD {v0, v1, v2, v3, v4} = 5 /\\r
1797      packing {v0, v1, v2, v3, v4} /\\r
1798      (!v. v IN {v1, v2, v3, v4} ==> d3 v0 v <= #2.51) /\\r
1799      quadp v0 v1 v2 v3 v4 /\\r
1800      d3 v1 v3 < sqrt8 /\\r
1801      d3 v2 v4 < sqrt8\r
1802      ==> d3 v1 v2 <= #2.51 /\\r
1803          d3 v2 v3 <= #2.51 /\\r
1804          d3 v3 v4 <= #2.51 /\\r
1805          d3 v1 v4 <= #2.51`;;\r
1806 let LEMMA128 = HTYDGWI;;\r
1807 (* le 129. p 79 *)\r
1808 let XLHACRX = ` !v0 v1 v2 v3 v4 w.\r
1809      CARD {v0, v1, v2, v3, v4, w} = 6 /\\r
1810      packing {v0, v1, v2, v3, v4, w} /\\r
1811      (!x. x IN {v1, v2, v3, v4} ==> d3 v0 x <= #2.51) /\\r
1812      quadp v0 v1 v2 v3 v4 /\\r
1813      d3 v1 v3 < sqrt8 /\\r
1814      d3 v2 v4 < sqrt8 /\\r
1815      w IN quadc0 v0 v1 v2 v3 v4 /\\r
1816      d3 w v0 < sqrt8\r
1817      ==> (!x. x IN {v1, v2, v3, v4} ==> d3 w x <= #2.51)`;;\r
1818 let LEMMA129 = XLHACRX;;\r
1819 \r
1820 let c_def38 = new_definition ` c_def38 S v' v1 v2 v3 v4 h1 h2 h3 h4 l k\r
1821   = ( CARD ({v', v1, v2, v3, v4} UNION S) = 5 + CARD S /\\r
1822  packing ({v', v1, v2, v3, v4} UNION S) /\\r
1823  quadp v' v1 v2 v3 v4 /\\r
1824  S SUBSET quadc0 v' v1 v2 v3 v4 /\\r
1825  (!vi. vi IN {v1, v2, v3, v4} ==> &2 <= d3 vi v' /\ d3 vi v' <= k) /\\r
1826  d3 v1 v2 <= k /\\r
1827  d3 v2 v3 <= k /\\r
1828  d3 v3 v4 <= k /\\r
1829  d3 v4 v1 <= k /\\r
1830  &2 <= d3 v1 v2 /\\r
1831  &2 <= d3 v2 v3 /\\r
1832  &2 <= d3 v3 v4 /\\r
1833  &2 <= d3 v4 v1 /\\r
1834  &2 <= d3 v1 v3 /\\r
1835  &2 <= d3 v2 v4 /\\r
1836  (!v. v IN S\r
1837       ==> &2 <= d3 v v' /\\r
1838           d3 v v' <= l /\\r
1839           h1 <= d3 v v1 /\\r
1840           h2 <= d3 v v2 /\\r
1841           h3 <= d3 v v3 /\\r
1842           h4 <= d3 v v4) )`;;\r
1843 \r
1844 \r
1845 g ` ! h1 h2 h3 h4 l k. \r
1846   (! x. x IN {h1,h2,h3,h4,l } ==> &2 <= x /\ x <= sqrt8 ) /\\r
1847   #2.51 <= k /\ k <= #2.517 /\\r
1848   c_def38 S v' v1 v2 v3 v4 h1 h2 h3 h4 l k /\\r
1849   h `;;\r
1850 (* le 131 . p 80 *)\r
1851 let GMEPVPW = ` ! k. #2.51 <= k /\\r
1852  k <= #2.517 /\\r
1853  ~(?v0 v1 v2 v3 v4 (w1:real^3) w2.\r
1854        CARD {v0, v1, v2, v3, v4, w1, w2} = 7 /\\r
1855        packing {v0, v1, v2, v3, v4, w1, w2} /\\r
1856        c_def38 {w1, w2} v0 v1 v2 v3 v4 (&2) (&2) (&2) (&2) k k /\\r
1857        (!vv. vv IN {v1, v2, v3, v4} ==> d3 v0 vv <= k) /\\r
1858        d3 v1 v2 <= k /\\r
1859        d3 v2 v3 <= k /\\r
1860        d3 v3 v4 <= k /\\r
1861        d3 v4 v1 <= k)`;;\r
1862 let LEMMA131 = GMEPVPW;;\r
1863 \r
1864 \r
1865 \r
1866 (* le 132 . p 80 *)\r
1867 let VTIVSIF = ` !v0 (v1:real^3) v2 v3 v4 v5.\r
1868      CARD {v0, v1, v2, v3, v4, v5} = 6 /\\r
1869      packing {v0, v1, v2, v3, v4, v5} /\\r
1870      quadp v0 v1 v2 v3 v4 /\\r
1871      v5 IN quadc0 v0 v1 v2 v3 v4 /\\r
1872      (!vv. vv IN {v1, v2, v3, v4} ==> d3 v0 vv <= #2.51) /\\r
1873      d3 v1 v2 <= #2.51 /\\r
1874      d3 v2 v3 <= #2.51 /\\r
1875      d3 v3 v4 <= #2.51 /\\r
1876      d3 v4 v1 <= #2.51 /\\r
1877      (!xx. xx IN {v2, v3, v4} ==> #2.51 <= d3 v5 xx)\r
1878      ==> #2.51 < d3 v0 v5`;;\r
1879 \r
1880 let LEMMA132 = VTIVSIF;;\r
1881 \r
1882 (* le 133 . p 81 *)\r
1883 let TPXUMUZ = ` !v0 v1 v2 v3 v4 v5.\r
1884      CARD {v0, v1, v2, v3, v4, v5} = 6 /\\r
1885      packing {v0, v1, v2, v3, v4, v5} /\\r
1886      quadp v0 v1 v2 v3 v4 /\\r
1887      v5 IN quadc0 v0 v1 v2 v3 v4 /\\r
1888      (!u v.\r
1889           {u, v} SUBSET {v0, v1, v2, v3, v4, v5} /\\r
1890           ~({u, v} = {v1, v3} \/\r
1891             {u, v} = {v2, v4} \/\r
1892             {u, v} = {v5, v4} \/\r
1893             {u, v} = {v5, v3})\r
1894           ==> d3 u v <= #2.51) /\\r
1895      #2.51 <= d3 v5 v3 /\\r
1896      #2.51 <= d3 v5 v4\r
1897      ==> (d3 v5 v4 <= sqrt8 \/ d3 v5 v3 <= sqrt8) /\\r
1898          (d3 v5 v4 <= #3.02 /\ d3 v5 v3 <= #3.02) /\\r
1899          #2.3 <= d3 v5 v0 `;;\r
1900 \r
1901 let LEMMA133 = TPXUMUZ;;\r
1902 \r
1903 \r
1904 (* le 134. p 82 *)\r
1905 \r
1906 let YWPHYZU = ` !v0 v1 v2 v3 v4 v5.\r
1907      CARD {v0, v1, v2, v3, v4, v5} = 6 /\\r
1908      packing {v0, v1, v2, v3, v4, v5} /\\r
1909      d3 v0 v5 < sqrt8 /\\r
1910      (!u v. u IN {v0, v5} /\ v IN {v1, v2} ==> d3 u v <= #2.51) /\\r
1911      ~(conv {v3, v4} INTER conv {v0, v1, v5} = {}) /\\r
1912      ~(conv {v3, v4} INTER conv {v0, v2, v5} = {})\r
1913      ==> sqrt8 < d3 v3 v4`;;\r
1914 \r
1915 let LEMMA134 = YWPHYZU;;\r
1916 \r
1917 (* le 135 . p 82 *)\r
1918 \r
1919 let PYURAKS = ` !v0 w w' v1 v2 v3.\r
1920      CARD {v0, w, w', v1, v2, v3} = 6 /\\r
1921      packing {v0, w, w', v1, v2, v3} /\\r
1922      d3 v1 v2 < sqrt8 /\\r
1923      d3 v1 v3 <= #2.51 /\\r
1924      d3 v2 v3 <= #2.51 /\\r
1925      {w, w'} SUBSET cone v0 {v1, v2, v3} /\\r
1926      d3 v0 w <= sqrt8\r
1927      ==> sqrt8 < d3 v0 w'`;;\r
1928 \r
1929 let LEMMA135 = PYURAKS;;\r
1930 \r
1931 \r
1932 \r
1933 let small = new_definition ` small s = \r
1934  ( CARD s = 3 /\\r
1935          packing s /\\r
1936          (!x y. {(x:real^3) , y} SUBSET s ==> d3 x y < sqrt8) /\\r
1937          (!x y z.\r
1938               {x, y, z} = s /\ #2.51 < d3 x y /\ #2.51 < d3 y z\r
1939               ==> radV s < sqrt (&2)) ) `;;\r
1940 (* le 136 . p *)\r
1941 \r
1942 let BLATMSI = ` !v1 v2 v3 v4 w w' s.\r
1943   CARD {v1, v2, v3, v4, w, w'} = 6 /\\r
1944      packing {v1, v2, v3, v4, w, w'} /\\r
1945      s = {v1, v2, v3, v4} /\\r
1946      (!v. v IN s ==> small (s DELETE v)) /\\r
1947      ~(conv {w, w'} INTER conv s = {}) /\\r
1948      d3 w w' < sqrt8\r
1949      ==> ~(conv {w, w'} INTER conv0 s = {})`;;\r
1950 \r
1951 let LEMMA136 = BLATMSI;;\r
1952 \r
1953 (* le 137. p 84 *)\r
1954 \r
1955 let MLTDJJV = ` !v1 v2 v3 v0 w w' s.\r
1956      CARD {v1, v2, v3, v0, w, w'} = 6 /\\r
1957      packing {v1, v2, v3, v0, w, w'} /\\r
1958      s = {v1, v2, v3, v0} /\\r
1959      d3 w w' < sqrt8 /\\r
1960      (!v. v IN s ==> small (s DELETE v)) /\\r
1961      (!x y. {x, y} SUBSET {v1, v2, v3} ==> d3 x y <= #2.51)\r
1962      ==> conv {w, w'} INTER conv s = {} `;;\r
1963 \r
1964 let LEMMA137 = MLTDJJV;;\r
1965 \r
1966 \r
1967 (* le 138 . p 85 *)\r
1968 let ZDKDXFM = ` !v0 v1 v2 v3 w w'.\r
1969      CARD {v0, v1, v2, v3, w, w'} = 6 /\\r
1970      packing {v0, v1, v2, v3, w, w'} /\\r
1971      d3 w w' < sqrt8 /\\r
1972      (!v. v IN {v0, v1, v2, v3} ==> small ({v0, v1, v2, v3} DELETE v)) /\\r
1973      #2.51 < d3 v1 v3 /\\r
1974      #2.51 < d3 v2 v0 /\\r
1975      ~(conv {w, w'} INTER conv0 {v0, v1, v2, v3} = {})\r
1976      ==> #2.51 < d3 w w' /\\r
1977          (!u vi. u IN {w, w'} /\ vi IN {v0, v1, v2, v3} ==> d3 u vi <= #2.51)`;;\r
1978 \r
1979 (* le 139 . 85 *)\r
1980 let XHMHKIZ = ` !v0 v1 v2 v3 w.\r
1981      CARD {v0, v1, v2, v3, w} = 5 /\\r
1982      packing {v0, v1, v2, v3, w} /\\r
1983      (!x y. {x, y} SUBSET {v1, v2, v3} ==> d3 x y <= sqrt8) /\\r
1984      ~(conv {v0, w} INTER conv0 {v0, v1, v2, v3} = {})\r
1985      ==> ~(conv {v0, w} INTER conv0 {v1, v2, v3} = {})`;;\r
1986 \r
1987 (* le 140 . p 86 *)\r
1988 let TIMIDQM = ` !v0 v1 v2 w0 w1 w2 x.\r
1989      CARD {v0, v1, v2, w0, w1, w2} = 6 /\\r
1990      packing {v0, v1, v2, w0, w1, w2} /\\r
1991      small {v0, v1, v2} /\\r
1992      small {w0, w1, w2} /\\r
1993      x IN conv {v0, v1, v2} INTER conv {w0, w1, w2}\r
1994      ==> (?v0' v1' v2' w0' w1' w2'.\r
1995               {v0, v1, v2} = {v0', v1', v2'} /\\r
1996               {w0, w1, w2} = {w0', w1', w2'} /\\r
1997               d3 w0' w1' <= #2.51 /\\r
1998               d3 w1' w2' <= #2.51 /\\r
1999               #2.51 < d3 w0' w2' /\\r
2000               d3 v0' v2' < sqrt8 /\\r
2001               d3 v0' v1' <= #2.51 /\\r
2002               d3 v1' v2' <= #2.51 /\\r
2003               #2.51 < d3 v0' v2' /\\r
2004               d3 v0' v2' < sqrt8 /\\r
2005               ~(conv {v0', v2'} INTER {w0, w1, w2} = {}) /\\r
2006               ~(conv {w0', w2'} INTER {v0, v1, v2} = {}))`;;\r
2007 \r
2008 let LEMMA140 = TIMIDQM;;\r
2009 \r
2010 (* le 141 . p 87 *)\r
2011 \r
2012 \r
2013 let KGTJGLX = ` !u0 v1 v2 w1 w2.\r
2014      CARD {u0, v1, v2, w1, w2} = 5 /\\r
2015      packing {u0, v1, v2, w1, w2} /\\r
2016      small {u0, v1, v2} /\\r
2017      small {u0, w1, w2} /\\r
2018      ~(conv0 {u0, v1, v2} INTER conv0 {u0, w1, w2} = {})\r
2019      ==> ~(conv {v1, v2} INTER conv {u0, w1, w2} = {} /\\r
2020            conv {w1, w2} INTER conv {u0, v1, v2} = {})`;;\r
2021 \r
2022 let LEMMA141 = KGTJGLX;;\r
2023 \r
2024 (* le 142 . p 87 *)\r
2025 \r
2026 let RTBONNT = ` !v1 v2 v3 v4 w1 w2 w3.\r
2027      CARD {v1, v2, v3, v4, w1, w2, w3} = 7 /\\r
2028      packing {v1, v2, v3, v4, w1, w2, w3} /\\r
2029      Sv = {v1, v2, v3, v4} /\\r
2030      Sw = {w1, w2, w3} /\\r
2031      small Sw /\\r
2032      (!v. v IN Sv ==> small (Sv DELETE v))\r
2033      ==> conv Sv INTER conv Sw = {}`;;\r
2034 \r
2035 let LEMMA142 = RTBONNT ;;\r
2036 \r
2037 (* le 143 . p88 *)\r
2038 \r
2039 \r
2040 let JMHCAKG = ` !v1 v2 v3 v4 w1 w2 w3.\r
2041      let sv = {v1, v2, v3, v4} in\r
2042      let sw = {w1, w2, w3} in\r
2043      let s = {v1, v2, v3, v4, w1, w2} in\r
2044      v1 = w1 /\\r
2045      CARD s = 6 /\\r
2046      packing s /\\r
2047      small sw /\\r
2048      (!v. v IN sv ==> small (sv DELETE v)) /\\r
2049      (?vv. ~(vv = v1) /\ vv IN conv sv INTER conv sw)\r
2050      ==> (?ww1 ww2 ww3 vv1 vv2 vv3 vv4.\r
2051               {ww1, ww2, ww3} = {w1, w2, w3} /\\r
2052               {vv1, vv2, vv3, vv4} = {v1, v2, v3, v4} /\\r
2053               ~(conv {ww1, ww3} INTER conv {vv2, vv3, vv4} = {}) /\\r
2054               ~(conv {vv2, vv4} INTER conv {ww1, ww2, ww3} = {}) /\\r
2055               #2.51 < d3 ww1 ww3 /\\r
2056               #2.51 < d3 vv2 vv4 /\\r
2057               d3 ww1 vv4 <= #2.51 /\\r
2058               d3 vv4 ww3 <= #2.51 /\\r
2059               d3 ww3 vv2 <= #2.51 /\\r
2060               d3 vv2 ww1 <= #2.51) \/\r
2061          (?ww1 ww2 ww3 vv1 vv2 vv3 vv4.\r
2062               {ww1, ww2, ww3} = {w1, w2, w3} /\\r
2063               {vv1, vv2, vv3, vv4} = {v1, v2, v3, v4} /\\r
2064               (?vi vj.\r
2065                    ~(vi = vj) /\\r
2066                    {vi, vj} SUBSET sv /\\r
2067                    ~(conv {ww2, ww3} INTER conv (sv DELETE vi) = {} \/\r
2068                      conv {ww2, ww3} INTER conv (sv DELETE vj) = {})) /\\r
2069               #2.51 < d3 vv2 vv3 /\\r
2070               #2.51 < d3 vv1 vv3 /\\r
2071               (!wi vj. wi IN {ww2, ww3} /\ vj IN sv ==> d3 wi vj <= #2.51))`;;\r
2072 \r
2073 let LEMMA143 = JMHCAKG ;;\r
2074 \r
2075 \r
2076 (* le 144. p 89 *)\r
2077 let UGQMJJA = `!v1 v2 v3 v4 w3 w1 w2.\r
2078      CARD {v1, v2, v3, v4, w1} = 5 /\\r
2079      packing {v1, v2, v3, v4, w1} /\\r
2080      w1 = v1 /\\r
2081      w2 = v2 /\\r
2082      sv = {v1, v2, v3, v4} /\\r
2083      sw = {w1, w2, w3} /\\r
2084      small sw /\\r
2085      (!v. v IN sv ==> small (sv DELETE v)) /\\r
2086      (?x. ~(x IN conv {v1, v2}) /\ x IN conv sv INTER conv sw)\r
2087      ==> (?ww1 vv2.\r
2088               {ww1, vv2} = {w1, v2} /\\r
2089               ~(conv {ww1, w3} INTER conv {vv2, v3, v4} = {}) /\\r
2090               #2.51 < d3 ww1 w3) \/\r
2091          ~(conv {v3, v4} INTER conv sw = {}) /\ #2.51 < d3 v3 v4`;;\r
2092 \r
2093 let LEMMA144 = UGQMJJA;;\r
2094 \r
2095 \r
2096 (* le 145. p 89 *)\r
2097 let ZILQMDQ = ` !v1 v2 v3 v4 w1 w2 w3 w4.\r
2098      let sv = {v1, v2, v3, v4} in\r
2099      let sw = {w1, w2, w3, w4} in\r
2100      CARD {v1, v2, v3, v4, w1, w2, w3, w4} = 8 /\\r
2101      packing {v1, v2, v3, v4, w1, w2, w3, w4} /\\r
2102      (!v. v IN sv ==> small (sv DELETE v)) /\\r
2103      (!w. w IN sw ==> small (sw DELETE w))\r
2104      ==> conv sv INTER conv sw = {}`;;\r
2105 \r
2106 let LEMMA145 = ZILQMDQ ;;\r
2107 \r
2108 \r
2109 (* le 146. p 90 *)\r
2110 \r
2111 let AQKANYN = ` !v1 v2 v3 v4 w1 w2 w3 w4.\r
2112      let sv = {v1, v2, v3, v4} in\r
2113      let sw = {w1, w2, w3, w4} in\r
2114      CARD {v1, v2, v3, v4, w2, w3, w4} = 7 /\\r
2115      packing {v1, v2, v3, v4, w2, w3, w4} /\\r
2116      w1 = v1 /\\r
2117      (!v. v IN sv ==> small (sv DELETE v)) /\\r
2118      (!w. w IN sw ==> small (sw DELETE w))\r
2119      ==> conv sv INTER conv sw = {v1}`;;\r
2120 \r
2121 \r
2122 let LEMMA146 = AQKANYN;;