Require Import ssreflect.
Require Import Reals.

Open Scope R_scope.

Notation "`| x |" := (Rabs x) (at level 0, format "`| x |") : 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, `|f x| <= 1) ->
  forall y, `|g y| <= 1.
Proof.
move=> f g Efg Hf0 Hf1 y; apply: Rnot_lt_le => Hgy1.
pose absf z := exists x, z = `|f x|.
have{Hf1} [k [Hub_k Hlub_k]]: {k : R & is_lub absf k}.
  by apply completeness; [exists 1 => _ [x ->] | exists `|f 1|; exists 1].
have{Hub_k} Hfk: `|f _| <= k by move=> x; apply: Hub_k; exists x.
have{Efg}: is_upper_bound absf (k / `|g y|).
  have Hgy0: 0 < `|g y| by exact: Rlt_trans Rlt_0_1 Hgy1.
  have H02 := Rlt_R0_R2; have Egy0 := sym_not_equal (Rlt_not_eq _ _ Hgy0).
  move=> _ [x ->]; apply: Rmult_le_reg_l Hgy0 _; rewrite Rmult_comm /Rdiv.
  rewrite -Rmult_assoc Rinv_r_simpl_m {Egy0}//; apply: Rmult_le_reg_l (H02) _.
  rewrite -{1}[2]Rabs_right; last by apply Rle_ge; exact: Rlt_le.
  rewrite double -!Rabs_mult -Rmult_assoc -Efg.
  by eapply Rle_trans; [apply Rabs_triang | apply Rplus_le_compat].
move/Hlub_k {Hlub_k}; case/Rle_not_lt; rewrite -{2}[k]Rmult_1_r -Rinv_1.
apply: Rmult_lt_compat_l; last by apply: Rinv_1_lt_contravar; first exact: Rle_refl.
apply: Rnot_le_lt => Hk; case: Hf0 => x; case (Req_dec (f x) 0); first done.
move/Rabs_pos_lt; case/Rlt_not_le; exact: Rle_trans Hk.
Qed.

End IMO.