Require Import Reals.
Require Import Fourier.

Open Scope R_scope.

Definition Rfbound (f: R -> R) b := forall x, (Rabs (f x) <= b).

(* Least upper bound for function *)
Theorem Rflub_def:
 forall f: R -> R, 
 forall b: R, Rfbound f b -> 
 exists k, 
    (Rfbound f k) /\ (forall b1, (Rfbound f b1) -> k <= b1).
intros f b Hb.
case (completeness (fun x => exists y, x = (Rabs (f y)))); auto.
exists b; red.
intros x [y Hy]; rewrite Hy; auto.
exists (Rabs (f 0)); exists 0; auto.
intros k [Hk1 Hk2]; exists k; split; auto.
  intros x; apply Hk1; exists x; auto.
intros b1 Hb1; apply Hk2.
intros x [y Hy]; rewrite Hy; auto.
Qed.

(* Tactic fields and fourier are first extended *)
Ltac ffield :=
  field; try apply Rmult_integral_contrapositive; 
  try split; try intros tmp; fourier.

Ltac ffourier := (split_Rabs; auto; fourier; fail).

(* Ready for the main theorem *)
Theorem imo1972:
 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 Eq Nz Rf1 y.
case (Rle_or_lt (Rabs (g y)) 1); intros H; auto.
case (Rflub_def f _ Rf1); clear Rf1.
intros k [Kb Kl].
assert (Kp: 0 < k); [idtac | clear Nz].
 case (Rle_or_lt k 0); auto; intros H1.
 case Nz; intros x.
 assert (HH: forall x, Rabs x = 0 -> x = 0);
  [intros x1; ffourier | idtac].
 apply HH; clear HH. 
 apply Rle_antisym; [idtac | apply Rabs_pos].
 assert (HH := Kb x); ffourier.
replace (Rabs (g y)) with (k * (Rabs(g y) / k));
  [idtac | ffield; auto with real].
replace 1 with (k / Rabs (g y) * (Rabs (g y) / k));
  [idtac | ffield].
apply Rmult_le_compat_r; auto.
unfold Rdiv; apply Rle_mult_inv_pos; auto with real;
  apply Rabs_pos.
apply Kl; clear Kl Kp.
intros x.
replace (Rabs (f x)) with
    (((2 * Rabs (g y) * Rabs (f x))) * (1/(2 * Rabs (g y))));
   [idtac | ffield].
replace (k / Rabs (g y)) with 
   ((2 * k) * (1/(2 * Rabs (g y)))); [idtac | ffield].
apply Rmult_le_compat_r; auto with real.
  apply (Rle_mult_inv_pos 1 (2 * Rabs (g y))); fourier.
pattern 2 at 1; rewrite <- (Rabs_pos_eq 2); auto with real.
repeat rewrite <- Rabs_mult.
replace (2 * g y * f x) with (2 * f x * g y); [idtac | ffield].
rewrite <- Eq; clear Eq.
assert (Bxpy := Kb (x + y));  assert (Bxmy := Kb (x - y));
  clear H Kb; ffourier.
Qed.