Require Import ssreflect.
Require Import Reals.

Open Scope R_scope.

Lemma IMO : forall f g,
  (forall x y, f (x + y) + f (x - y) = 2 * f x * g y) ->
  ~ (forall x, f x = 0) ->
  (forall x, Rabs (f x) <= 1) ->
  forall y, Rabs (g y) <= 1.
Proof.
move=> f g Efg Hf0 Hf1 y; apply Rnot_lt_le => Hy1.
have Hy0:= Rlt_trans _ _ _ Rlt_0_1 Hy1.
have Ey0: g y <> 0 by move=> Dy; case/Rlt_not_eq: Hy0; rewrite Dy Rabs_R0.
case Hf0 => x; apply cond_eq => k; case/(pow_lt_1_zero (/ g y)) => [|n Hn].
  by apply: Rmult_lt_reg_l Hy0 _; rewrite -Rabs_mult Rmult_1_r Rinv_r // Rabs_R1.
rewrite Rminus_0_r; apply: Rle_lt_trans {Hn}(Hn n (le_n n)).
elim: n x => [|n IHn] x /=; [ by rewrite Rabs_R1 | apply: Rmult_le_reg_l Hy0 _].
rewrite -!Rabs_mult Rmult_comm -Rmult_assoc Rinv_r // Rmult_1_l.
apply: Rmult_le_reg_l Rlt_R0_R2 _.
rewrite -{1}[2](Rabs_Zabs 2) -Rabs_mult -Rmult_assoc -Efg double.
apply: Rle_trans (Rabs_triang _ _) _; exact: Rplus_le_compat.
Qed.