Section OrderedAlgDefs.

Variable R : Type.
Variable z o : R.
Notation "0" := z.
Notation "1" := o.
Variable p : R -> R -> R.
Notation "s + t" := (p s t).
Variable m : R -> R -> R.
Notation "s * t" := (m s t).
Variable n : R -> R.
Variable r : R -> R.
Variable le : R -> R -> Prop.
Notation "s <= t" := (le s t).

Variable eq : R -> R -> Prop.
Notation "s == t" := (eq s t)(at level 70, no associativity).

Variable l : R -> R -> Prop.
Notation "s < t" := (l s t).

Implicit Type x y z a b c: R.
Implicit Type S T: R->Prop.

Definition reflexive : Prop :=
forall x, x == x.

Definition symmetric : Prop :=
forall x y, x == y -> y == x.

Definition transitive : Prop :=
forall x y z, x == y -> y == z -> x == z.

Definition commutative : Prop :=
forall x y, x + y = y + x.

Definition associative : Prop :=
forall x y z, (x + y) + z = x + (y + z).

Definition ac_twist : Prop :=
forall x y z, x + (y + z) = (x + z) + y.

Definition plus_irreflexive : Prop :=
forall x y, x <> y + x.

Definition identity_l : Prop :=
forall x, 0 + x = x.

Definition identity_r : Prop :=
forall x, x + 0 = x.

Definition exist_inv_l : Prop :=
forall x, exists y, y + x = 0.

Definition exist_inv_l_ex : Prop :=
forall x, x <> 0 -> exists y, y * x = 1.

Definition exist_inv_r : Prop :=
forall x, exists y, x + y = 0.

Definition exist_solns_1 : Prop :=
forall x y, exists z, x = y + z.

Definition exist_solns_2 : Prop :=
forall x y, y <> 0 -> exists z, x = y * z.

Definition distributes : Prop :=
forall x y z, x * (y + z) = (x * y) + (x * z).

Definition inverse_exception_l : Prop :=
forall x, x <> 0 -> (r x) * x = 1.

Definition inverse_l : Prop :=
forall x, (r x) * x = 1.

Definition linear : Prop :=
forall x y, x <= y \/ y <= x.

Definition trichotomy : Prop :=
forall x y, x < y \/ x = y \/ y < x.

Definition irreflexive : Prop :=
forall x, x < x -> False.

Definition asymmetric : Prop :=
forall x y, x < y -> y < x -> False.

Definition antisymmetric : Prop :=
forall x y, x <= y -> y <= x -> x = y.

Definition dense : Prop :=
forall x z, x < z -> exists y, x < y /\ y < z.

Definition less_plus : Prop :=
forall x y z t, x + z < y + t -> x < y \/ z < t.

Definition less_plus_1 : Prop :=
forall x y z, y < z -> x + y < x + z.

Definition less_plus_2 : Prop :=
forall a b c, a <= b -> a + c <= b + c.

Definition less_mult : Prop :=
forall x y z, 0 < x -> y < z -> x * y < x * z.

Definition less_mult_2 : Prop :=
forall a b c, a <= b -> a * c <= b * c.

Definition less_mult_pos : Prop :=
forall a b, 0 <= a -> 0 <= b -> 0 <= a * b.

Definition eq_plus_injective : Prop :=
forall a b c, a + c = b + c -> a = b.

Definition noendp_r : Prop :=
forall a, exists b, a < b.

Definition noendp_l : Prop :=
forall a, exists b, b < a.

Definition annihilates_l : Prop :=
forall a, 0 * a = 0.

Definition annihilates_r : Prop :=
forall a, a * 0 = 0.

Definition discrete : Prop :=
forall x, 0 <= x -> x <= 1 -> x = 0 \/ x = 1.

Definition one_less_two : Prop :=
1 < 1 + 1.

Definition zero_not_one : Prop :=
0 <> 1.

Definition TAcompleteness : Prop :=
forall S T, (forall x y, S x -> T y -> x < y)
       -> (exists z, forall x y, S x -> T y -> x <> z -> y <> z -> x < z /\ z < y).


Definition ub p x := forall y, p y -> y < x \/ y = x.

Definition sup p x := ub p x /\ forall y, ub p y -> x < y \/ x = y.

Definition HAsupremum : Prop := forall p, ex p -> ex (ub p) -> ex (sup p).

Fixpoint iter (R : Type) (p : R -> R -> R) (x : R) (n : nat)
:= match n with O => x | S n => p (iter R p x n) x end.

Definition JDarchimedean : Prop :=
forall x:R, le z x -> z <> x -> forall y:R, le z y -> exists
n:nat, le y (iter R p x n).

Definition JDnestedIntervals : Prop :=
forall a b:nat -> R,
(forall n:nat, le (a n) (b n) /\ le (a n) (a (S n)) /\ le (b (S n)) (b n))
-> exists x:R, forall n:nat, le (a n) x /\ le x (b n).


Definition inductionaxiom : Prop :=
forall S, S 1 -> (forall x, S x -> S (x+1)) -> forall x, S x.

Definition NaturalNumbers_minimal : Prop :=
forall S:R -> Prop, S o
 -> (forall x y, S x -> S y -> S (x + y))
 -> (forall x y, S x -> S y -> S (x * y))
 -> forall x, S x.

Definition PositiveRational_minimal : Prop :=
forall S:R -> Prop, S o
 -> (forall x y, S x -> S y -> S (x + y))
 -> (forall x y, S x -> S y -> S (x * y))
 -> (forall x, S x -> S (r x))
 -> forall x, S x.

Definition Integer_minimal : Prop :=
forall S:R -> Prop, S z -> S o
 -> (forall x y, S x -> S y -> S (x + y))
 -> (forall x, S x -> S (n x))
 -> forall x, S x.

Definition Rational_minimal : Prop :=
forall S:R -> Prop, S z -> S o
 -> (forall x y, S x -> S y -> S (x + y))
 -> (forall x y, S x -> S y -> S (x * y))
 -> (forall x, S x -> S (n x))
 -> (forall x, S x -> x <> 0 -> S (r x))
 -> forall x, S x.

End OrderedAlgDefs.