Require Import ZArith.
Require Import PolTac.

Open Scope Z_scope.

Theorem pols_test1: forall (x y : Z), x < y ->  (x + x < y + x).
(* Goal: forall (x y : Z) (_ : Z.lt Z0 x) (_ : Z.le x (Z.mul x y)), Z.le (Zpos xH) y *)
intros.
(* Goal: Z.le (Z.add y y) (Z.mul (Zpos (xO xH)) y) *)
pols.
(* Goal: Z.lt (Z.add x z) y *)
(* Goal: Z.le (Z.add y y) (Z.mul (Zpos (xO xH)) y) *)
auto.
Qed.
 
Theorem pols_test2: forall (x y : Z), y < 0 ->  (x + y < x).
(* Goal: forall (x y : Z) (_ : Z.lt Z0 x) (_ : Z.le x (Z.mul x y)), Z.le (Zpos xH) y *)
intros.
(* Goal: Z.le (Z.add y y) (Z.mul (Zpos (xO xH)) y) *)
pols.
(* Goal: Z.lt (Z.add x z) y *)
(* Goal: Z.le (Z.add y y) (Z.mul (Zpos (xO xH)) y) *)
auto.
Qed.
 
Theorem pols_test3: forall (x y : Z), 0 < y * y ->  ((x + y) * (x - y) < x * x).
(* Goal: forall (x y : Z) (_ : Z.lt Z0 x) (_ : Z.le x (Z.mul x y)), Z.le (Zpos xH) y *)
intros.
(* Goal: Z.le (Z.add y y) (Z.mul (Zpos (xO xH)) y) *)
pols.
(* Goal: Z.le Z0 Z0 *)
auto with zarith.
Qed.
 
Theorem pols_test4:
 forall (x y : Z),
 x * x  < y * y ->  ((x + y) * (x + y) < 2 * (x * y + y * y)).
(* Goal: forall (x y : Z) (_ : Z.lt Z0 x) (_ : Z.le x (Z.mul x y)), Z.le (Zpos xH) y *)
intros.
(* Goal: Z.le (Z.add y y) (Z.mul (Zpos (xO xH)) y) *)
pols.
(* Goal: Z.lt (Z.add x z) y *)
(* Goal: Z.le (Z.add y y) (Z.mul (Zpos (xO xH)) y) *)
auto.
Qed.
 
Theorem pols_test5:
 forall x y z, x + y * (y + z) = 2 * z ->  2 * x + y * (y + z) = (x + z) + z.
(* Goal: forall (x y : Z) (_ : Z.lt Z0 x) (_ : Z.le x (Z.mul x y)), Z.le (Zpos xH) y *)
intros.
(* Goal: Z.le (Z.add y y) (Z.mul (Zpos (xO xH)) y) *)
pols.
(* Goal: Z.lt (Z.add x z) y *)
(* Goal: Z.le (Z.add y y) (Z.mul (Zpos (xO xH)) y) *)
auto.
Qed.

Theorem polf_test1: forall x y, (0 <= x -> 1 <= y -> x  <= x  * y)%Z.
(* Goal: forall (x y : Z) (_ : Z.lt Z0 x) (_ : Z.le x (Z.mul x y)), Z.le (Zpos xH) y *)
intros.
(* Goal: Z.le x (Z.mul x y) *)
polf.
Qed.

Theorem polf_test2: forall x y, (0 < x -> x  <= x  * y -> 1 <= y)%Z.
(* Goal: forall (x y : Z) (_ : Z.lt Z0 x) (_ : Z.le x (Z.mul x y)), Z.le (Zpos xH) y *)
intros.
(* Goal: Z.le (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 : Z) (_ : Z.lt (Z.add x z) y), Z.lt (Z.add (Z.add x y) z) (Z.mul (Zpos (xO xH)) y) *)
intros x y z H.
(* Goal: Z.lt (Z.add (Z.add x y) z) (Z.mul (Zpos (xO xH)) y) *)
polr H.
(* Goal: Z.le (Z.add y y) (Z.mul (Zpos (xO xH)) y) *)
pols.
(* Goal: Z.lt (Z.add x z) y *)
(* Goal: Z.le (Z.add y y) (Z.mul (Zpos (xO xH)) y) *)
auto.
(* Goal: Z.le (Z.add y y) (Z.mul (Zpos (xO xH)) y) *)
pols.
(* Goal: Z.le Z0 Z0 *)
auto with zarith.
Qed.
