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.