Require Import PolTac.
Require Import ZArith.

(* Test for Z *)
Open Scope  Z_scope.

Ltac cg g := match goal with |- g => idtac end.


Goal forall a b c d, a + c = d -> b + d = c + d -> a + b + c = c + d.
(* Goal: forall (a b c d : Z) (_ : Z.le (Z.add a c) d) (_ : Z.le b c), Z.le (Z.add (Z.add a b) c) (Z.add c d) *)
intros a b c d H1 H2.
(* Goal: Z.le (Z.add (Z.add a b) c) (Z.add c d) *)
polr H1.
(* Goal: @eq Z (Z.add c Z0) (Z.add c d) *)
(* Goal: @eq Z (Z.add (Z.add a b) c) (Z.add c Z0) *)
rewrite H1; auto. 
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, d = 0 -> a + b + c = c + 0 -> a + b + c = c + d.
(* Goal: forall (a b c d : Z) (_ : Z.le (Z.add a c) d) (_ : Z.le b c), Z.le (Z.add (Z.add a b) c) (Z.add c d) *)
intros a b c d H1 H2.
(* Goal: Z.le (Z.add (Z.add a b) c) (Z.add c d) *)
polr H1.
(* Goal: @eq Z (Z.add c Z0) (Z.add c d) *)
(* Goal: @eq Z (Z.add (Z.add a b) c) (Z.add c Z0) *)
rewrite H1; auto.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c <= d -> b <= c -> a + b + c <= c + d.
(* Goal: forall (a b c d : Z) (_ : Z.le (Z.add a c) d) (_ : Z.le b c), Z.le (Z.add (Z.add a b) c) (Z.add c d) *)
intros a b c d H1 H2.
(* Goal: Z.le (Z.add (Z.add a b) c) (Z.add c d) *)
polr H1.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d,  a + b  <= 0 -> 0 <= d -> a + b + c <= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c >= d -> b >= c -> a + b + c >= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + b >= 0 -> 0 >= d -> a + b + c >= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.


Goal forall a b c d, a + c < d -> b <= c -> a + b + c < c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + b <= 0 -> 0 < d -> a + b + c < c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c > d -> c <= b -> a + b + c > c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, 0 <= a + b -> 0 > d -> a + b + c > c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

(* Test for N *)
Require Import NAux.
Open Scope  N_scope.

Goal forall a b c d, a + c = d -> b = c -> a + b + c = c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: @eq R (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c = d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, 0 = d -> a + b = 0 -> a + b + c = c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: @eq R (Rplus (Rplus a b) c) (Rplus c d) *)
polr (d = 0).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c <= d -> b <= c -> a + b + c <= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + b <= 0 -> 0 <= d -> a + b + c <= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c >= d -> b >= c -> a + b + c >= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + b >= 0 -> 0 >= d -> a + b + c >= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c < d -> b <= c -> a + b + c < c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + b <= 0 -> 0 < d -> a + b + c < c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c > d -> c <= b -> a + b + c > c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, 0 <= a + b -> 0 > d -> a + b + c > c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Require Import Arith.
(* Test for Nat *)
Open Scope  nat_scope.

Goal forall a b c d, a + c = d -> b = c -> a + b + c = c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: @eq R (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c = d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, 0 = d -> a + b = 0 -> a + b + c = c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: @eq R (Rplus (Rplus a b) c) (Rplus c d) *)
polr (d = 0).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c <= d -> b <= c -> a + b + c <= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + b <= 0 -> 0 <= d -> a + b + c <= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c <= d -> b <= c -> a + b + c <= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + b >= 0 -> 0 >= d -> a + b + c >= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z. 
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c < d -> b <= c -> a + b + c < c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + b <= 0 -> 0 < d -> a + b + c < c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c > d -> c <= b -> a + b + c > c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(*
NatPolR.npolrx (a + c < d) P.L P.L 1%Z.
*)
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, 0 <= a + b -> 0 > d -> a + b + c > c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

(* Test for R *)
Require Import Reals.
Open Scope  R_scope.

Goal forall a b c d, a + c = d -> b = c -> a + b + c = c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: @eq R (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c = d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, 0 = d -> a + b = 0 -> a + b + c = c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: @eq R (Rplus (Rplus a b) c) (Rplus c d) *)
polr (d = 0).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c <= d -> b <= c -> a + b + c <= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + b <= 0 -> 0 <= d -> a + b + c <= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c >= d -> b >= c -> a + b + c >= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + b >= 0 -> 0 >= d -> a + b + c >= c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.

Goal forall a b c d, a + c < d -> b <= c -> a + b + c < c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.
 
Goal forall a b c d, a + b <= 0 -> 0 < d -> a + b + c < c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed. 

Goal forall a b c d, a + c > d -> b >= c -> a + b + c > c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polr (a + c < d).
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed. 

Goal forall a b c d, a + b >= 0 -> 0 > d -> a + b + c > c + d.
(* Goal: forall (a b c d : R) (_ : Rge (Rplus a b) (IZR Z0)) (_ : Rgt (IZR Z0) d), Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
intros.
(* Goal: Rgt (Rplus (Rplus a b) c) (Rplus c d) *)
polrx (0 < d) P.R P.R 1%Z.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
(* Goal: Rgt (Rplus c (IZR Z0)) (Rplus c d) *)
pols.
(* Goal: Rgt (IZR Z0) d *)
auto.
Qed.
