Library Coq.Numbers.Integer.Abstract.ZLt


Require Export ZMul.

Module ZOrderProp (Import Z : ZAxiomsMiniSig´).
Include ZMulProp Z.

Instances of earlier theorems for m == 0

Theorem neg_pos_cases : forall n, n ~= 0 <-> n < 0 \/ n > 0.

Theorem nonpos_pos_cases : forall n, n <= 0 \/ n > 0.

Theorem neg_nonneg_cases : forall n, n < 0 \/ n >= 0.

Theorem nonpos_nonneg_cases : forall n, n <= 0 \/ n >= 0.

Ltac zinduct n := induction_maker n ltac:(apply order_induction_0).

Theorems that are either not valid on N or have different proofs on N and Z

Theorem lt_pred_l : forall n, P n < n.

Theorem le_pred_l : forall n, P n <= n.

Theorem lt_le_pred : forall n m, n < m <-> n <= P m.

Theorem nle_pred_r : forall n, ~ n <= P n.

Theorem lt_pred_le : forall n m, P n < m <-> n <= m.

Theorem lt_lt_pred : forall n m, n < m -> P n < m.

Theorem le_le_pred : forall n m, n <= m -> P n <= m.

Theorem lt_pred_lt : forall n m, n < P m -> n < m.

Theorem le_pred_lt : forall n m, n <= P m -> n <= m.

Theorem pred_lt_mono : forall n m, n < m <-> P n < P m.

Theorem pred_le_mono : forall n m, n <= m <-> P n <= P m.

Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m.

Theorem le_succ_le_pred : forall n m, S n <= m <-> n <= P m.

Theorem lt_pred_lt_succ : forall n m, P n < m <-> n < S m.

Theorem le_pred_lt_succ : forall n m, P n <= m <-> n <= S m.

Theorem neq_pred_l : forall n, P n ~= n.

Theorem lt_m1_r : forall n m, n < m -> m < 0 -> n < -1.

End ZOrderProp.