Require Import Reals.
Require Import PolTac.

Open Scope R_scope.
 
Theorem pols_test1: forall (x y : R), x < y ->  (x + x < y + x).
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rle x (Rmult x y)), Rle (IZR (Zpos xH)) y *)
intros.
(* Goal: Rle (Rplus u y) (Rplus y u) *)
pols.
(* Goal: Rlt (Rplus x z) y *)
(* Goal: Rle (Rplus u y) (Rplus y u) *)
auto.
Qed.
 
Theorem pols_test2: forall (x y : R), 0 < y ->  (x  < x + y).
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rle x (Rmult x y)), Rle (IZR (Zpos xH)) y *)
intros.
(* Goal: Rle (Rplus u y) (Rplus y u) *)
pols.
(* Goal: Rlt (Rplus x z) y *)
(* Goal: Rle (Rplus u y) (Rplus y u) *)
auto.
Qed.
 
Theorem pols_test3: forall (x y : R), 0 < y * y ->  ((x + y) * (x - y) < x * x).
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rle x (Rmult x y)), Rle (IZR (Zpos xH)) y *)
intros.
(* Goal: Rle (Rplus u y) (Rplus y u) *)
pols.
(* Goal: Rle (IZR Z0) (IZR Z0) *)
auto with real.
Qed.

Theorem pols_test4:
 forall (x y : R),
 x * x  < y * y ->  ((x + y) * (x + y) < 2 * (x * y + y * y)).
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rle x (Rmult x y)), Rle (IZR (Zpos xH)) y *)
intros.
(* Goal: Rle (Rplus u y) (Rplus y u) *)
pols.
(* Goal: Rlt (Rplus x z) y *)
(* Goal: Rle (Rplus u y) (Rplus y u) *)
auto.
Qed.
 
Theorem pols_test5:
 forall (x y z : R),
 x * (z + 2) < y * (2 * x + 1)->  (x * ((z + y) + 2) < y * (3 * x + 1)).
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rle x (Rmult x y)), Rle (IZR (Zpos xH)) y *)
intros.
(* Goal: Rle (Rplus u y) (Rplus y u) *)
pols.
(* Goal: Rlt (Rplus x z) y *)
(* Goal: Rle (Rplus u y) (Rplus y u) *)
auto.
Qed.

Theorem polf_test1: forall x y, (0 <= x -> 1 <= y -> x  <=  x  * y)%R.
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rle x (Rmult x y)), Rle (IZR (Zpos xH)) y *)
intros.
(* Goal: Rlt (Rmult (Rmult (IZR (Zpos (xO xH))) y) t) (Rplus (Rplus (Rmult x t) (Rmult t u)) (Rmult z t)) *)
polf.
Qed.

Theorem polf_test2: forall x y, (0 < x -> x  <= x  * y -> 1 <= y)%R.
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rle x (Rmult x y)), Rle (IZR (Zpos xH)) y *)
intros.
(* Goal: Rle (IZR (Zpos xH)) y *)
hyp_polf H0.
Qed.

Theorem polr_test1: forall x y z, (x + z) < y -> x + y + z < 2*y.
(* Goal: forall (x y z : R) (_ : Rlt (Rplus x z) y), Rlt (Rplus (Rplus x y) z) (Rmult (IZR (Zpos (xO xH))) y) *)
intros x y z H.
(* Goal: Rlt (Rplus (Rplus x y) z) (Rmult (IZR (Zpos (xO xH))) y) *)
polr H.
(* Goal: Rle (Rplus u y) (Rplus y u) *)
pols.
(* Goal: Rlt (Rplus x z) y *)
(* Goal: Rle (Rplus u y) (Rplus y u) *)
auto.
(* Goal: Rle (Rplus u y) (Rplus y u) *)
pols.
(* Goal: Rle (IZR Z0) (IZR Z0) *)
auto with real.
Qed.

Theorem polr_test2: forall x y z t u, t <0 -> y = u -> x + z <  y ->  2* y * t <  x * t + t * u + z * t .
(* Goal: forall (x y z t u : R) (_ : Rlt t (IZR Z0)) (_ : @eq R y u) (_ : Rlt (Rplus x z) y), Rlt (Rmult (Rmult (IZR (Zpos (xO xH))) y) t) (Rplus (Rplus (Rmult x t) (Rmult t u)) (Rmult z t)) *)
intros x y z t u H H1 H2.
(* Goal: Rlt (Rmult (Rmult (IZR (Zpos (xO xH))) y) t) (Rplus (Rplus (Rmult x t) (Rmult t u)) (Rmult z t)) *)
polf.
(* Goal: Rle (IZR Z0) (IZR Z0) *)
polr H1; auto with real.
(* Goal: Rlt (Rplus (Rplus x u) z) (Rplus y u) *)
polr H2.
(* Goal: Rle (Rplus u y) (Rplus y u) *)
pols.
(* Goal: Rlt (Rplus x z) y *)
(* Goal: Rle (Rplus u y) (Rplus y u) *)
auto.
(* Goal: Rle (Rplus u y) (Rplus y u) *)
pols.
(* Goal: Rle (IZR Z0) (IZR Z0) *)
auto with real.
Qed.


