needs "Multivariate/misc.ml";;

let LEMMA1 = prove
 (`(!x y. f(x + y) + f(x - y) = &2 * f(x) * g(y)) /\ (!x. abs(f x) <= &1)
   ==> !l x. abs(f x * (g y) pow l) <= &1`,
  DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN INDUCT_TAC THEN
  ASM_SIMP_TAC[real_pow; REAL_MUL_RID] THEN GEN_TAC THEN MATCH_MP_TAC
   (REAL_ARITH `abs((&2 * a * b) * c) <= &2 ==> abs(a * b * c) <= &1`) THEN
  ASM_SIMP_TAC[] THEN FIRST_ASSUM(MP_TAC o SPEC `x + y`) THEN
  FIRST_ASSUM(MP_TAC o SPEC `x - y`) THEN REAL_ARITH_TAC);;

let LEMMA2 = prove
 (`~(x = &0) /\ &1 < abs(y) ==> ?n. &1 < abs(y pow n * x)`,
  SIMP_TAC[REAL_ABS_MUL; REAL_ABS_POW; GSYM REAL_LT_LDIV_EQ;
           GSYM REAL_ABS_NZ; REAL_ARCH_POW]);;

let IMO = prove
 (`!f g. (!x y. f(x + y) + f(x - y) = &2 * f(x) * g(y)) /\
         ~(!x. f(x) = &0) /\
         (!x. abs(f(x)) <= &1)
         ==> !x. abs(g(x)) <= &1`,
  MESON_TAC[LEMMA1; LEMMA2; REAL_NOT_LE; REAL_MUL_SYM]);;