Library Coq.Numbers.Integer.Abstract.ZLt



Require Export ZMul.

Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
Module Export ZMulPropMod := ZMulPropFunct ZAxiomsMod.
Open Local Scope IntScope.


Theorem Zlt_wd :
  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 < m1 <-> n2 < m2).
Theorem Zle_wd :
  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 <= m1 <-> n2 <= m2).
Theorem Zmin_wd :
  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmin n1 m1 == Zmin n2 m2.
Theorem Zmax_wd :
  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmax n1 m1 == Zmax n2 m2.
Theorem Zlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n == m.
Theorem Zlt_irrefl : forall n : Z, ~ n < n.
Theorem Zlt_succ_r : forall n m : Z, n < S m <-> n <= m.
Theorem Zmin_l : forall n m : Z, n <= m -> Zmin n m == n.
Theorem Zmin_r : forall n m : Z, m <= n -> Zmin n m == m.
Theorem Zmax_l : forall n m : Z, m <= n -> Zmax n m == n.
Theorem Zmax_r : forall n m : Z, n <= m -> Zmax n m == m.
Theorem Zlt_le_incl : forall n m : Z, n < m -> n <= m.
Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m.
Theorem Zle_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m.
Theorem Zle_refl : forall n : Z, n <= n.
Theorem Zlt_succ_diag_r : forall n : Z, n < S n.
Theorem Zle_succ_diag_r : forall n : Z, n <= S n.
Theorem Zlt_0_1 : 0 < 1.
Theorem Zle_0_1 : 0 <= 1.
Theorem Zlt_lt_succ_r : forall n m : Z, n < m -> n < S m.
Theorem Zle_le_succ_r : forall n m : Z, n <= m -> n <= S m.
Theorem Zle_succ_r : forall n m : Z, n <= S m <-> n <= m \/ n == S m.
Theorem Zneq_succ_diag_l : forall n : Z, S n ~= n.
Theorem Zneq_succ_diag_r : forall n : Z, n ~= S n.
Theorem Znlt_succ_diag_l : forall n : Z, ~ S n < n.
Theorem Znle_succ_diag_l : forall n : Z, ~ S n <= n.
Theorem Zle_succ_l : forall n m : Z, S n <= m <-> n < m.
Theorem Zlt_succ_l : forall n m : Z, S n < m -> n < m.
Theorem Zsucc_lt_mono : forall n m : Z, n < m <-> S n < S m.
Theorem Zsucc_le_mono : forall n m : Z, n <= m <-> S n <= S m.
Theorem Zlt_asymm : forall n m, n < m -> ~ m < n.
Notation Zlt_ngt := Zlt_asymm (only parsing).

Theorem Zlt_trans : forall n m p : Z, n < m -> m < p -> n < p.
Theorem Zle_trans : forall n m p : Z, n <= m -> m <= p -> n <= p.
Theorem Zle_lt_trans : forall n m p : Z, n <= m -> m < p -> n < p.
Theorem Zlt_le_trans : forall n m p : Z, n < m -> m <= p -> n < p.
Theorem Zle_antisymm : forall n m : Z, n <= m -> m <= n -> n == m.
Theorem Zlt_1_l : forall n m : Z, 0 < n -> n < m -> 1 < m.
Trichotomy, decidability, and double negation elimination
Theorem Zlt_trichotomy : forall n m : Z, n < m \/ n == m \/ m < n.
Notation Zlt_eq_gt_cases := Zlt_trichotomy (only parsing).

Theorem Zlt_gt_cases : forall n m : Z, n ~= m <-> n < m \/ n > m.
Theorem Zle_gt_cases : forall n m : Z, n <= m \/ n > m.
Theorem Zlt_ge_cases : forall n m : Z, n < m \/ n >= m.
Theorem Zle_ge_cases : forall n m : Z, n <= m \/ n >= m.
Instances of the previous theorems for m == 0
Theorem Zneg_pos_cases : forall n : Z, n ~= 0 <-> n < 0 \/ n > 0.

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

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

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

Theorem Zle_ngt : forall n m : Z, n <= m <-> ~ n > m.
Theorem Znlt_ge : forall n m : Z, ~ n < m <-> n >= m.
Theorem Zlt_dec : forall n m : Z, decidable (n < m).
Theorem Zlt_dne : forall n m, ~ ~ n < m <-> n < m.
Theorem Znle_gt : forall n m : Z, ~ n <= m <-> n > m.
Theorem Zlt_nge : forall n m : Z, n < m <-> ~ n >= m.
Theorem Zle_dec : forall n m : Z, decidable (n <= m).
Theorem Zle_dne : forall n m : Z, ~ ~ n <= m <-> n <= m.
Theorem Znlt_succ_r : forall n m : Z, ~ m < S n <-> n < m.
Theorem Zlt_exists_pred :
  forall z n : Z, z < n -> exists k : Z, n == S k /\ z <= k.
Theorem Zlt_succ_iter_r :
  forall (n : nat) (m : Z), m < NZsucc_iter (Datatypes.S n) m.
Theorem Zneq_succ_iter_l :
  forall (n : nat) (m : Z), NZsucc_iter (Datatypes.S n) m ~= m.
Stronger variant of induction with assumptions n >= 0 (n < 0) in the induction step
Theorem Zright_induction :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    forall z : Z, A z ->
      (forall n : Z, z <= n -> A n -> A (S n)) ->
        forall n : Z, z <= n -> A n.
Theorem Zleft_induction :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    forall z : Z, A z ->
      (forall n : Z, n < z -> A (S n) -> A n) ->
        forall n : Z, n <= z -> A n.
Theorem Zright_induction' :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    forall z : Z,
      (forall n : Z, n <= z -> A n) ->
      (forall n : Z, z <= n -> A n -> A (S n)) ->
        forall n : Z, A n.
Theorem Zleft_induction' :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    forall z : Z,
    (forall n : Z, z <= n -> A n) ->
    (forall n : Z, n < z -> A (S n) -> A n) ->
      forall n : Z, A n.
Theorem Zstrong_right_induction :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    forall z : Z,
    (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
       forall n : Z, z <= n -> A n.
Theorem Zstrong_left_induction :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    forall z : Z,
      (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
        forall n : Z, n <= z -> A n.
Theorem Zstrong_right_induction' :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    forall z : Z,
      (forall n : Z, n <= z -> A n) ->
      (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
        forall n : Z, A n.
Theorem Zstrong_left_induction' :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    forall z : Z,
    (forall n : Z, z <= n -> A n) ->
    (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
      forall n : Z, A n.
Theorem Zorder_induction :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    forall z : Z, A z ->
    (forall n : Z, z <= n -> A n -> A (S n)) ->
    (forall n : Z, n < z -> A (S n) -> A n) ->
      forall n : Z, A n.
Theorem Zorder_induction' :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    forall z : Z, A z ->
    (forall n : Z, z <= n -> A n -> A (S n)) ->
    (forall n : Z, n <= z -> A n -> A (P n)) ->
      forall n : Z, A n.
Theorem Zorder_induction_0 :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    A 0 ->
    (forall n : Z, 0 <= n -> A n -> A (S n)) ->
    (forall n : Z, n < 0 -> A (S n) -> A n) ->
      forall n : Z, A n.
Theorem Zorder_induction'_0 :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    A 0 ->
    (forall n : Z, 0 <= n -> A n -> A (S n)) ->
    (forall n : Z, n <= 0 -> A n -> A (P n)) ->
      forall n : Z, A n.
Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction_0).
Elimintation principle for <
Theorem Zlt_ind :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    forall n : Z, A (S n) ->
      (forall m : Z, n < m -> A m -> A (S m)) -> forall m : Z, n < m -> A m.
Elimintation principle for <=
Theorem Zle_ind :
  forall A : Z -> Prop, predicate_wd Zeq A ->
    forall n : Z, A n ->
      (forall m : Z, n <= m -> A m -> A (S m)) -> forall m : Z, n <= m -> A m.
Well-founded relations
Theorem Zlt_wf : forall z : Z, well_founded (fun n m : Z => z <= n /\ n < m).
Theorem Zgt_wf : forall z : Z, well_founded (fun n m : Z => m < n /\ n <= z).
Theorem Zlt_pred_l : forall n : Z, P n < n.

Theorem Zle_pred_l : forall n : Z, P n <= n.

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

Theorem Znle_pred_r : forall n : Z, ~ n <= P n.

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

Theorem Zlt_lt_pred : forall n m : Z, n < m -> P n < m.

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

Theorem Zlt_pred_lt : forall n m : Z, n < P m -> n < m.

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

Theorem Zpred_lt_mono : forall n m : Z, n < m <-> P n < P m.

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

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

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

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

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

Theorem Zneq_pred_l : forall n : Z, P n ~= n.

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

End ZOrderPropFunct.