Require Export ZLt.

Module ZAddOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod.
Open Local Scope IntScope.

Theorem Zadd_lt_mono_l : forall n m p : Z, n < m <-> p + n < p + m.

Theorem Zadd_lt_mono_r : forall n m p : Z, n < m <-> n + p < m + p.

Theorem Zadd_lt_mono : forall n m p q : Z, n < m -> p < q -> n + p < m + q.

Theorem Zadd_le_mono_l : forall n m p : Z, n <= m <-> p + n <= p + m.

Theorem Zadd_le_mono_r : forall n m p : Z, n <= m <-> n + p <= m + p.

Theorem Zadd_le_mono : forall n m p q : Z, n <= m -> p <= q -> n + p <= m + q.

Theorem Zadd_lt_le_mono : forall n m p q : Z, n < m -> p <= q -> n + p < m + q.

Theorem Zadd_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q.

Theorem Zadd_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n + m.

Theorem Zadd_pos_nonneg : forall n m : Z, 0 < n -> 0 <= m -> 0 < n + m.

Theorem Zadd_nonneg_pos : forall n m : Z, 0 <= n -> 0 < m -> 0 < n + m.

Theorem Zadd_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n + m.

Theorem Zlt_add_pos_l : forall n m : Z, 0 < n -> m < n + m.

Theorem Zlt_add_pos_r : forall n m : Z, 0 < n -> m < m + n.

Theorem Zle_lt_add_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q.

Theorem Zlt_le_add_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q.

Theorem Zle_le_add_le : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q.

Theorem Zadd_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q.

Theorem Zadd_le_cases : forall n m p q : Z, n + m <= p + q -> n <= p \/ m <= q.

Theorem Zadd_neg_cases : forall n m : Z, n + m < 0 -> n < 0 \/ m < 0.

Theorem Zadd_pos_cases : forall n m : Z, 0 < n + m -> 0 < n \/ 0 < m.

Theorem Zadd_nonpos_cases : forall n m : Z, n + m <= 0 -> n <= 0 \/ m <= 0.

Theorem Zadd_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m.

Theorem Zadd_neg_neg : forall n m : Z, n < 0 -> m < 0 -> n + m < 0.

Theorem Zadd_neg_nonpos : forall n m : Z, n < 0 -> m <= 0 -> n + m < 0.

Theorem Zadd_nonpos_neg : forall n m : Z, n <= 0 -> m < 0 -> n + m < 0.

Theorem Zadd_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> n + m <= 0.

Sub and order

Theorem Zlt_0_sub : forall n m : Z, 0 < m - n <-> n < m.

Notation Zsub_pos := Zlt_0_sub (only parsing).

Theorem Zle_0_sub : forall n m : Z, 0 <= m - n <-> n <= m.

Notation Zsub_nonneg := Zle_0_sub (only parsing).

Theorem Zlt_sub_0 : forall n m : Z, n - m < 0 <-> n < m.

Notation Zsub_neg := Zlt_sub_0 (only parsing).

Theorem Zle_sub_0 : forall n m : Z, n - m <= 0 <-> n <= m.

Notation Zsub_nonpos := Zle_sub_0 (only parsing).

Theorem Zopp_lt_mono : forall n m : Z, n < m <-> - m < - n.

Theorem Zopp_le_mono : forall n m : Z, n <= m <-> - m <= - n.

Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0.

Theorem Zopp_neg_pos : forall n : Z, - n < 0 <-> 0 < n.

Theorem Zopp_nonneg_nonpos : forall n : Z, 0 <= - n <-> n <= 0.

Theorem Zopp_nonpos_nonneg : forall n : Z, - n <= 0 <-> 0 <= n.

Theorem Zsub_lt_mono_l : forall n m p : Z, n < m <-> p - m < p - n.

Theorem Zsub_lt_mono_r : forall n m p : Z, n < m <-> n - p < m - p.

Theorem Zsub_lt_mono : forall n m p q : Z, n < m -> q < p -> n - p < m - q.

Theorem Zsub_le_mono_l : forall n m p : Z, n <= m <-> p - m <= p - n.

Theorem Zsub_le_mono_r : forall n m p : Z, n <= m <-> n - p <= m - p.

Theorem Zsub_le_mono : forall n m p q : Z, n <= m -> q <= p -> n - p <= m - q.

Theorem Zsub_lt_le_mono : forall n m p q : Z, n < m -> q <= p -> n - p < m - q.

Theorem Zsub_le_lt_mono : forall n m p q : Z, n <= m -> q < p -> n - p < m - q.

Theorem Zle_lt_sub_lt : forall n m p q : Z, n <= m -> p - n < q - m -> p < q.

Theorem Zlt_le_sub_lt : forall n m p q : Z, n < m -> p - n <= q - m -> p < q.

Theorem Zle_le_sub_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q.

Theorem Zlt_add_lt_sub_r : forall n m p : Z, n + p < m <-> n < m - p.

Theorem Zle_add_le_sub_r : forall n m p : Z, n + p <= m <-> n <= m - p.

Theorem Zlt_add_lt_sub_l : forall n m p : Z, n + p < m <-> p < m - n.

Theorem Zle_add_le_sub_l : forall n m p : Z, n + p <= m <-> p <= m - n.

Theorem Zlt_sub_lt_add_r : forall n m p : Z, n - p < m <-> n < m + p.

Theorem Zle_sub_le_add_r : forall n m p : Z, n - p <= m <-> n <= m + p.

Theorem Zlt_sub_lt_add_l : forall n m p : Z, n - m < p <-> n < m + p.

Theorem Zle_sub_le_add_l : forall n m p : Z, n - m <= p <-> n <= m + p.

Theorem Zlt_sub_lt_add : forall n m p q : Z, n - m < p - q <-> n + q < m + p.

Theorem Zle_sub_le_add : forall n m p q : Z, n - m <= p - q <-> n + q <= m + p.

Theorem Zlt_sub_pos : forall n m : Z, 0 < m <-> n - m < n.

Theorem Zle_sub_nonneg : forall n m : Z, 0 <= m <-> n - m <= n.

Theorem Zsub_lt_cases : forall n m p q : Z, n - m < p - q -> n < m \/ q < p.

Theorem Zsub_le_cases : forall n m p q : Z, n - m <= p - q -> n <= m \/ q <= p.

Theorem Zsub_neg_cases : forall n m : Z, n - m < 0 -> n < 0 \/ 0 < m.

Theorem Zsub_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0.

Theorem Zsub_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m.

Theorem Zsub_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0.

Section PosNeg.

Variable P : Z -> Prop.
Hypothesis P_wd : predicate_wd Zeq P.

Add Morphism P with signature Zeq ==> iff as P_morph. Proof. Qed.

Theorem Z0_pos_neg :
P 0 -> (forall n : Z, 0 < n -> P n /\ P (- n)) -> forall n : Z, P n.

End PosNeg.

Ltac Z0_pos_neg n := induction_maker n ltac:(apply Z0_pos_neg).