Library positivereduced

Require Import Arith.
Require Import ZArith.
Require Import Omega.
Require Import Bool.
Eval compute in andb true false.
Eval compute in (3<5).

Open Scope Z_scope.

Print Zabs.

Definition reduced (a b c d:Z):Prop :=
(Zabs a + Zabs c <= Zabs(a-b) + Zabs(c-d))/\
(Zabs b + Zabs d <= Zabs(a-b) + Zabs(c-d))/\
(Zabs(a-b) + Zabs(c-d) <= Zabs(a+b) + Zabs(c+d))
.
Print reduced.

Definition extrareduced (a b c d:Z):Prop :=
(reduced a b c d)/\
Zabs b<=a /\ Zabs c<=a /\ d<=a /\
0<=d /\
(Zabs b=d -> Zabs c<d)
.
Print extrareduced.

Definition reducedsigns (a b c d:Z):Prop :=
d<=a /\ Zabs b<=d /\ Zabs c<=d /\
2*b+c<=a /\
2*c+b<=d /\
0<=b+c /\
(Zabs b=d -> Zabs c<d)
.



Lemma zabsgt0 : forall a, 0<=Zabs a.

Lemma zabsgreater : forall a, a<=Zabs a.

Lemma zabsgreaterthan : forall a b,
Zabs b<=a -> b<=a.

Lemma zgtmakeabs : forall a b,
a<=b -> -a<=b -> Zabs a<=b.

Lemma a2bctoabbc : forall a b c,
c<=a -> 2*b+c<=a -> Zabs b+b+c<=a.

Theorem reducedhassigns : forall a b c d,
(extrareduced a b c d)<->(reducedsigns a b c d).