Require Import Reals. Require Import Fourier. Require Import Classical. Open Scope R_scope. Definition Rfbound (f: R -> R) b := forall x, (Rabs (f x) <= b). Ltac ffourier := (split_Rabs; auto; fourier; fail). Theorem imo1972_hales: forall f g: R -> R, (forall x y: R, f (x + y) + f (x - y) = 2 * f x * g y) -> ~ (forall x: R, f x = 0) -> Rfbound f 1 -> Rfbound g 1. intros f g He Hp Hb. assert (He1: forall l x y, Rabs (2 * (f x * g y ^ l)) <= 2). induction l; simpl; [intros x y; rewrite Rmult_1_r; assert (Hu := Hb x); ffourier | idtac]. intros x y; repeat rewrite <- Rmult_assoc; rewrite <- He; rewrite Rmult_plus_distr_r. assert (tmp1 := IHl (x + y) y); assert (tmp2 := IHl (x - y) y). clear IHl; ffourier. case (not_all_ex_not R (fun n => f n = 0) Hp); intros x Hx; clear Hp Hb. intros y; clear He. case (Rle_or_lt (Rabs (g y)) 1); intros H; auto. case (Pow_x_infinity _ H (1 + 2/ Rabs (2 * f x))); intros x0 Hexp; clear H. assert (Hexp1 := Hexp x0 (le_refl x0)); clear Hexp. assert (Hexp2 := He1 x0 x y); clear He1. let x := (type of Hexp2) in absurd x; auto; clear Hexp2; apply Rgt_not_le; rewrite <- Rmult_assoc; rewrite Rabs_mult. assert (H1: Rabs (2 * f x) > 0). red; apply Rabs_pos_lt; apply prod_neq_R0; intros HH; try fourier; case Hx; auto. pattern 2 at 2; replace 2 with (Rabs (2 * f x) * (2 / Rabs (2 * f x))). red; apply Rmult_lt_compat_l; ffourier. field; auto with real. Qed.