100/minkowski.ml

   1 (* ========================================================================= *)
   2 (* Minkowski's convex body theorem.                                          *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/measure.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* An ad hoc lemma.                                                          *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let LEMMA = prove
  12  (`!f:real^N->bool t s:real^N->bool.
  13         FINITE { u | u IN f /\ ~(t u = {})} /\
  14         measurable s /\ &1 < measure s /\
  15         (!u. u IN f ==> measurable(t u)) /\
  16         s SUBSET UNIONS (IMAGE t f) /\
  17         (!u v. u IN f /\ v IN f /\ ~(u = v) ==> DISJOINT (t u) (t v)) /\
  18         (!u. u IN f ==> (IMAGE (\x. x - u) (t u)) SUBSET interval[vec 0,vec 1])
  19         ==> ?u v. u IN f /\ v IN f /\ ~(u = v) /\
  20                   ~(DISJOINT (IMAGE (\x. x - u) (t u))
  21                              (IMAGE (\x. x - v) (t v)))`,
  22   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [TAUT `p <=> ~ ~p`] THEN
  23   PURE_REWRITE_TAC[NOT_EXISTS_THM] THEN
  24   REWRITE_TAC[TAUT `~(a /\ b /\ ~c /\ ~d) <=> a /\ b /\ ~c ==> d`] THEN
  25   DISCH_TAC THEN
  26   MP_TAC(ISPECL [`\u:real^N. IMAGE (\x:real^N. x - u) (t u)`;
  27                  `f:real^N->bool`]
  28                 HAS_MEASURE_DISJOINT_UNIONS_IMAGE_STRONG) THEN
  29   ASM_REWRITE_TAC[IMAGE_EQ_EMPTY; NOT_IMP] THEN CONJ_TAC THENL
  30    [REWRITE_TAC[VECTOR_ARITH `x - u:real^N = --u + x`] THEN
  31     ASM_REWRITE_TAC[MEASURABLE_TRANSLATION_EQ];
  32     ALL_TAC] THEN
  33   MP_TAC(ISPECL [`vec 0:real^N`; `vec 1:real^N`] (CONJUNCT1
  34                 HAS_MEASURE_INTERVAL)) THEN
  35   REWRITE_TAC[CONTENT_UNIT] THEN
  36   MATCH_MP_TAC(TAUT `(b /\ a ==> F) ==> a ==> ~b`) THEN
  37   DISCH_THEN(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE
  38    [TAUT `a /\ b /\ c ==> d <=> a /\ b ==> c ==> d`] HAS_MEASURE_SUBSET)) THEN
  39   ASM_REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_IMAGE; REAL_NOT_LE] THEN
  40   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
  41    `&1 < a ==> a <= b ==> &1 < b`)) THEN
  42   MATCH_MP_TAC REAL_LE_TRANS THEN
  43   EXISTS_TAC `measure(UNIONS (IMAGE (t:real^N->real^N->bool) f))` THEN
  44   CONJ_TAC THENL
  45    [MATCH_MP_TAC MEASURE_SUBSET THEN ASM_REWRITE_TAC[] THEN
  46     SUBGOAL_THEN
  47      `UNIONS (IMAGE (t:real^N->real^N->bool) f) =
  48       UNIONS (IMAGE t {u | u IN f /\ ~(t u = {})})`
  49     SUBST1_TAC THENL
  50      [GEN_REWRITE_TAC I [EXTENSION] THEN
  51       REWRITE_TAC[IN_UNIONS; IN_IMAGE; IN_ELIM_THM] THEN
  52       MESON_TAC[NOT_IN_EMPTY];
  53       ALL_TAC] THEN
  54     MATCH_MP_TAC MEASURABLE_UNIONS THEN
  55     ASM_REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
  56     ASM_SIMP_TAC[FINITE_IMAGE; IN_ELIM_THM] THEN ASM_MESON_TAC[];
  57     ALL_TAC] THEN
  58   MP_TAC(ISPECL [`t:real^N->real^N->bool`; `f:real^N->bool`]
  59                 HAS_MEASURE_DISJOINT_UNIONS_IMAGE_STRONG) THEN
  60   ASM_REWRITE_TAC[IMAGE_EQ_EMPTY; NOT_IMP] THEN
  61   DISCH_THEN(SUBST1_TAC o MATCH_MP MEASURE_UNIQUE) THEN
  62   REWRITE_TAC[VECTOR_ARITH `x - u:real^N = --u + x`] THEN
  63   ASM_SIMP_TAC[MEASURE_TRANSLATION; REAL_LE_REFL]);;
  64
  65 (* ------------------------------------------------------------------------- *)
  66 (* This is also interesting, and Minkowski follows easily from it.           *)
  67 (* ------------------------------------------------------------------------- *)
  68
  69 let BLICHFELDT = prove
  70  (`!s:real^N->bool.
  71         bounded s /\ measurable s /\ &1 < measure s
  72         ==> ?x y. x IN s /\ y IN s /\ ~(x = y) /\
  73                   !i. 1 <= i /\ i <= dimindex(:N) ==> integer(x$i - y$i)`,
  74   REPEAT STRIP_TAC THEN
  75   MP_TAC(ISPECL [`{ u:real^N | !i. 1 <= i /\ i <= dimindex(:N)
  76                                    ==> integer(u$i) }`;
  77                  `\u. {x | (x:real^N) IN s /\
  78                            !i. 1 <= i /\ i <= dimindex(:N)
  79                                ==> (u:real^N)$i <= x$i /\ x$i < u$i + &1 }`;
  80                  `s:real^N->bool`]
  81                 LEMMA) THEN
  82   ASM_REWRITE_TAC[IN_ELIM_THM] THEN ANTS_TAC THENL
  83    [ALL_TAC;
  84     REWRITE_TAC[DISJOINT; GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM] THEN
  85     MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN
  86     REWRITE_TAC[EXISTS_IN_IMAGE; IN_INTER] THEN
  87     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  88     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:real^N` THEN
  89     REWRITE_TAC[IN_IMAGE; IN_ELIM_THM] THEN
  90     REWRITE_TAC[VECTOR_ARITH `x - u:real^N = y - v <=> x + (v - u) = y`] THEN
  91     REWRITE_TAC[UNWIND_THM1] THEN STRIP_TAC THEN
  92     EXISTS_TAC `x + (v - u):real^N` THEN
  93     ASM_REWRITE_TAC[VECTOR_ARITH `x = x + (v - u) <=> v:real^N = u`] THEN
  94     ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT] THEN
  95     ASM_SIMP_TAC[REAL_ARITH `x - (x + v - u) = u - v`; INTEGER_CLOSED]] THEN
  96   REPEAT CONJ_TAC THENL
  97    [SUBGOAL_THEN
  98      `?N. !x:real^N i. x IN s /\ 1 <= i /\ i <= dimindex(:N) ==> abs(x$i) < &N`
  99     STRIP_ASSUME_TAC THENL
 100      [FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [BOUNDED_POS]) THEN
 101       DISCH_THEN(X_CHOOSE_TAC `B:real`) THEN
 102       MP_TAC(SPEC `B:real` (MATCH_MP REAL_ARCH REAL_LT_01)) THEN
 103       MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[REAL_MUL_RID] THEN
 104       X_GEN_TAC `N:num` THEN
 105       REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NUM] THEN
 106       SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_LT_POW2] THEN
 107       ASM_MESON_TAC[COMPONENT_LE_NORM; REAL_LE_TRANS; REAL_LET_TRANS];
 108       ALL_TAC] THEN
 109     MATCH_MP_TAC FINITE_SUBSET THEN
 110     EXISTS_TAC
 111      `{u:real^N | !i. 1 <= i /\ i <= dimindex(:N)
 112                       ==> integer (u$i) /\ abs(u$i) <= &N}` THEN
 113     CONJ_TAC THENL
 114      [MATCH_MP_TAC FINITE_CART THEN
 115       REWRITE_TAC[GSYM REAL_BOUNDS_LE; FINITE_INTSEG];
 116       ALL_TAC] THEN
 117     REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN X_GEN_TAC `u:real^N` THEN
 118     STRIP_TAC THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN ASM_SIMP_TAC[] THEN
 119     MATCH_MP_TAC REAL_LE_REVERSE_INTEGERS THEN
 120     ASM_SIMP_TAC[INTEGER_CLOSED] THEN
 121     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
 122     REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
 123     X_GEN_TAC `y:real^N` THEN
 124     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `k:num`)) THEN
 125     FIRST_X_ASSUM(MP_TAC o SPECL [`y:real^N`; `k:num`]) THEN
 126     ASM_SIMP_TAC[] THEN REAL_ARITH_TAC;
 127     X_GEN_TAC `u:real^N` THEN DISCH_TAC THEN
 128     MATCH_MP_TAC MEASURABLE_ALMOST THEN
 129     EXISTS_TAC `s INTER interval[u:real^N,u + vec 1]` THEN
 130     ASM_SIMP_TAC[MEASURABLE_INTER_INTERVAL] THEN
 131     EXISTS_TAC `interval[u:real^N,u + vec 1] DIFF interval(u,u + vec 1)` THEN
 132     REWRITE_TAC[NEGLIGIBLE_FRONTIER_INTERVAL] THEN
 133     MATCH_MP_TAC(SET_RULE
 134      `s' SUBSET i /\ j INTER s' = j INTER s
 135       ==> (s INTER i) UNION (i DIFF j) = s' UNION (i DIFF j)`) THEN
 136     REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INTERVAL; IN_INTER; EXTENSION;
 137                 IN_ELIM_THM] THEN
 138     CONJ_TAC THEN X_GEN_TAC `x:real^N` THEN
 139     ASM_CASES_TAC `(x:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN TRY EQ_TAC THEN
 140     REWRITE_TAC[AND_FORALL_THM] THEN MATCH_MP_TAC MONO_FORALL THEN
 141     REWRITE_TAC[TAUT `(a ==> b) /\ (a ==> c) <=> a ==> b /\ c`] THEN
 142     GEN_TAC THEN DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
 143     ASM_SIMP_TAC[VECTOR_ADD_COMPONENT; VEC_COMPONENT] THEN REAL_ARITH_TAC;
 144     REWRITE_TAC[SUBSET; IN_UNIONS; EXISTS_IN_IMAGE; IN_ELIM_THM] THEN
 145     X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
 146     EXISTS_TAC `(lambda i. floor((x:real^N)$i)):real^N` THEN
 147     ASM_SIMP_TAC[LAMBDA_BETA; FLOOR];
 148     MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN
 149     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 150     ASM_SIMP_TAC[CART_EQ; REAL_EQ_INTEGERS] THEN
 151     REWRITE_TAC[NOT_FORALL_THM; LEFT_IMP_EXISTS_THM; NOT_IMP; REAL_NOT_LT] THEN
 152     X_GEN_TAC `k:num` THEN STRIP_TAC THEN REWRITE_TAC[DISJOINT] THEN
 153     REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY; IN_ELIM_THM] THEN
 154     REPEAT STRIP_TAC THEN
 155     REPEAT(FIRST_X_ASSUM (MP_TAC o SPEC `k:num`)) THEN
 156     ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
 157     X_GEN_TAC `u:real^N` THEN DISCH_THEN(K ALL_TAC) THEN
 158     REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM; IN_INTERVAL] THEN
 159     GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 160     MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
 161     SIMP_TAC[VECTOR_SUB_COMPONENT; VEC_COMPONENT] THEN
 162     MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN REAL_ARITH_TAC]);;
 163
 164 (* ------------------------------------------------------------------------- *)
 165 (* The usual form of the theorem.                                            *)
 166 (* ------------------------------------------------------------------------- *)
 167
 168 let MINKOWSKI = prove
 169  (`!s:real^N->bool.
 170         convex s /\
 171         bounded s /\
 172         (!x. x IN s ==> (--x) IN s) /\
 173         &2 pow dimindex(:N) < measure s
 174         ==> ?u. ~(u = vec 0) /\
 175                 (!i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)) /\
 176                 u IN s`,
 177   REPEAT STRIP_TAC THEN
 178   MP_TAC(ISPEC `IMAGE (\x:real^N. (&1 / &2) % x) s` BLICHFELDT) THEN
 179   ASM_SIMP_TAC[MEASURABLE_SCALING; MEASURE_SCALING; MEASURABLE_CONVEX;
 180                BOUNDED_SCALING] THEN
 181   REWRITE_TAC[real_div; REAL_MUL_LID; REAL_ABS_INV; REAL_ABS_NUM] THEN
 182   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 183   REWRITE_TAC[GSYM real_div; REAL_POW_INV] THEN
 184   ASM_SIMP_TAC[REAL_LT_RDIV_EQ; REAL_LT_POW2; REAL_MUL_LID] THEN
 185   REWRITE_TAC[RIGHT_EXISTS_AND_THM; EXISTS_IN_IMAGE] THEN
 186   REWRITE_TAC[VECTOR_ARITH `inv(&2) % x:real^N = inv(&2) % y <=> x = y`] THEN
 187   REWRITE_TAC[LEFT_IMP_EXISTS_THM; RIGHT_AND_EXISTS_THM] THEN
 188   SIMP_TAC[VECTOR_MUL_COMPONENT; GSYM REAL_SUB_LDISTRIB] THEN
 189   MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN
 190   EXISTS_TAC `inv(&2) % (u - v):real^N` THEN
 191   ASM_SIMP_TAC[VECTOR_ARITH `inv(&2) % (u - v):real^N = vec 0 <=> u = v`] THEN
 192   ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; VECTOR_SUB_COMPONENT] THEN
 193   REWRITE_TAC[VECTOR_SUB; VECTOR_ADD_LDISTRIB] THEN
 194   FIRST_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [convex]) THEN
 195   ASM_SIMP_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
 196
 197 (* ------------------------------------------------------------------------- *)
 198 (* A slightly sharper variant for use when the set is also closed.           *)
 199 (* ------------------------------------------------------------------------- *)
 200
 201 let MINKOWSKI_COMPACT = prove
 202  (`!s:real^N->bool.
 203         convex s /\ compact s /\
 204         (!x. x IN s ==> (--x) IN s) /\
 205         &2 pow dimindex(:N) <= measure s
 206         ==> ?u. ~(u = vec 0) /\
 207                 (!i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)) /\
 208                 u IN s`,
 209   GEN_TAC THEN ASM_CASES_TAC `s:real^N->bool = {}` THENL
 210    [ASM_REWRITE_TAC[GSYM REAL_NOT_LT; MEASURE_EMPTY; REAL_LT_POW2];
 211     ALL_TAC] THEN
 212   STRIP_TAC THEN
 213   SUBGOAL_THEN `(vec 0:real^N) IN s` ASSUME_TAC THENL
 214    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
 215     DISCH_THEN(X_CHOOSE_TAC `a:real^N`) THEN
 216     SUBST1_TAC(VECTOR_ARITH `vec 0:real^N = inv(&2) % a + inv(&2) % --a`) THEN
 217     FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [convex]) THEN
 218     ASM_SIMP_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV;
 219     ALL_TAC] THEN
 220   REPEAT STRIP_TAC THEN
 221   MP_TAC(ISPECL
 222     [`s:real^N->bool`;
 223      `{u | !i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)}
 224       DELETE (vec 0:real^N)`]
 225     SEPARATE_COMPACT_CLOSED) THEN
 226   REWRITE_TAC[EXTENSION; IN_DELETE; IN_ELIM_THM; IN_INTER; NOT_IN_EMPTY] THEN
 227   MATCH_MP_TAC(TAUT
 228    `(~e ==> c) /\ a /\ b /\ (d ==> e)
 229         ==> (a /\ b /\ c ==> d) ==> e`) THEN
 230   CONJ_TAC THENL [MESON_TAC[]; ASM_REWRITE_TAC[]] THEN CONJ_TAC THENL
 231    [MATCH_MP_TAC DISCRETE_IMP_CLOSED THEN
 232     EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01; IN_DELETE; IN_ELIM_THM] THEN
 233     REPEAT GEN_TAC THEN
 234     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
 235     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 236     REWRITE_TAC[CART_EQ; REAL_NOT_LT; NOT_FORALL_THM; NOT_IMP] THEN
 237     DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
 238     MATCH_MP_TAC REAL_LE_TRANS THEN
 239     EXISTS_TAC `abs((y - x:real^N)$k)` THEN
 240     ASM_SIMP_TAC[COMPONENT_LE_NORM; VECTOR_SUB_COMPONENT] THEN
 241     ASM_MESON_TAC[REAL_EQ_INTEGERS; REAL_NOT_LE];
 242     ALL_TAC] THEN
 243   SIMP_TAC[dist] THEN DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
 244   FIRST_ASSUM(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
 245   REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN
 246   X_GEN_TAC `B:real` THEN STRIP_TAC THEN
 247   MP_TAC(ISPEC `IMAGE (\x:real^N. (&1 + d / &2 / B) % x) s` MINKOWSKI) THEN
 248   ANTS_TAC THENL
 249    [ASM_SIMP_TAC[CONVEX_SCALING; BOUNDED_SCALING; COMPACT_IMP_BOUNDED] THEN
 250     ASM_SIMP_TAC[MEASURABLE_COMPACT; MEASURE_SCALING] THEN CONJ_TAC THENL
 251      [REWRITE_TAC[FORALL_IN_IMAGE; IN_IMAGE] THEN
 252       REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_ARITH
 253        `--(a % x):real^N = a % y <=> a % (x + y) = vec 0`] THEN
 254       ASM_MESON_TAC[VECTOR_ADD_RINV];
 255       ALL_TAC] THEN
 256     FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 257      `d <= m ==> m < n ==> d < n`)) THEN
 258     REWRITE_TAC[REAL_ARITH `m < a * m <=> &0 < m * (a - &1)`] THEN
 259     MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC THENL
 260      [ASM_SIMP_TAC[MEASURABLE_COMPACT; MEASURABLE_MEASURE_POS_LT] THEN
 261       REWRITE_TAC[GSYM HAS_MEASURE_0] THEN
 262       DISCH_THEN(SUBST_ALL_TAC o MATCH_MP MEASURE_UNIQUE) THEN
 263       ASM_MESON_TAC[REAL_NOT_LT; REAL_LT_POW2];
 264       ALL_TAC] THEN
 265     REWRITE_TAC[REAL_SUB_LT] THEN MATCH_MP_TAC REAL_POW_LT_1 THEN
 266     REWRITE_TAC[DIMINDEX_NONZERO] THEN
 267     MATCH_MP_TAC(REAL_ARITH `&0 < x ==> &1 < abs(&1 + x)`) THEN
 268     ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH];
 269     ALL_TAC] THEN
 270   ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> c /\ b /\ a`] THEN
 271   REWRITE_TAC[EXISTS_IN_IMAGE; VECTOR_MUL_EQ_0; DE_MORGAN_THM] THEN
 272   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:real^N` THEN
 273   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 274   FIRST_X_ASSUM(MP_TAC o SPECL
 275    [`u:real^N`; `(&1 + d / &2 / B) % u:real^N`]) THEN
 276   ASM_REWRITE_TAC[VECTOR_MUL_EQ_0] THEN
 277   REWRITE_TAC[VECTOR_ARITH `u - (&1 + e) % u:real^N = --(e % u)`] THEN
 278   REWRITE_TAC[NORM_NEG; NORM_MUL] THEN
 279   MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN REWRITE_TAC[REAL_NOT_LE] THEN
 280   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(d / &2 / B) * B` THEN
 281   ASM_SIMP_TAC[REAL_LE_LMUL; REAL_ABS_POS] THEN
 282   ASM_REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_NUM] THEN
 283   ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> abs x = x`] THEN
 284   ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_LT_IMP_NZ] THEN
 285   UNDISCH_TAC `&0 < d` THEN REAL_ARITH_TAC);;