needs "Multivariate/misc.ml";;

let IMO = prove
 (`!f g:real->real.
        (!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`,
  REPEAT STRIP_TAC THEN
  ABBREV_TAC `k = sup (IMAGE (\x. abs(f(x))) (:real))` THEN
  MP_TAC(SPEC `IMAGE (\x. abs(f(x))) (:real)` SUP) THEN
  ASM_REWRITE_TAC[FORALL_IN_IMAGE; EXISTS_IN_IMAGE; IN_UNIV] THEN
  ANTS_TAC THENL
   [CONJ_TAC THENL [SET_TAC[]; ASM_MESON_TAC[]]; ALL_TAC] THEN
  STRIP_TAC THEN SPEC_TAC(`x:real`,`y:real`) THEN
  REWRITE_TAC[REAL_ARITH `z <= &1 <=> ~(&1 < z)`] THEN
  REWRITE_TAC[GSYM NOT_EXISTS_THM] THEN STRIP_TAC THEN
  MP_TAC(ASSUME `!b. (!x:real. abs (f x) <= b) ==> k <= b`) THEN
  REWRITE_TAC[NOT_IMP; NOT_FORALL_THM] THEN
  EXISTS_TAC `k / abs(g(y:real))` THEN CONJ_TAC THENL
   [GEN_TAC THEN
    ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_ARITH `&1 < x ==> &0 < x`] THEN
    REWRITE_TAC[GSYM REAL_ABS_MUL] THEN
    MATCH_MP_TAC(REAL_ARITH
     `!u v. u + v = &2 * z /\ abs(u) <= k /\ abs(v) <= k
            ==> abs(z) <= k`) THEN
    ASM_MESON_TAC[];
    REWRITE_TAC[REAL_NOT_LE] THEN
    ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_ARITH `&1 < x ==> &0 < x`] THEN
    ASM_MESON_TAC[REAL_LT_LMUL; REAL_ARITH `x * &1 < y ==> x < y`;
    REAL_ARITH `!z. ~(z = &0) /\ abs(z) <= k ==> &0 < k`]]);;