Library Coq.Numbers.NatInt.NZOrder
Require Import NZAxioms.
Require Import NZMul.
Require Import Decidable.
Module NZOrderPropFunct (
Import NZOrdAxiomsMod :
NZOrdAxiomsSig).
Module Export NZMulPropMod :=
NZMulPropFunct NZAxiomsMod.
Open Local Scope NatIntScope.
Ltac le_elim H :=
rewrite NZlt_eq_cases in H;
destruct H as [
H |
H].
Theorem NZlt_le_incl :
forall n m :
NZ,
n <
m ->
n <=
m.
Theorem NZeq_le_incl :
forall n m :
NZ,
n ==
m ->
n <=
m.
Lemma NZlt_stepl :
forall x y z :
NZ,
x <
y ->
x ==
z ->
z <
y.
Lemma NZlt_stepr :
forall x y z :
NZ,
x <
y ->
y ==
z ->
x <
z.
Lemma NZle_stepl :
forall x y z :
NZ,
x <=
y ->
x ==
z ->
z <=
y.
Lemma NZle_stepr :
forall x y z :
NZ,
x <=
y ->
y ==
z ->
x <=
z.
Declare Left Step NZlt_stepl.
Declare Right Step NZlt_stepr.
Declare Left Step NZle_stepl.
Declare Right Step NZle_stepr.
Theorem NZlt_neq :
forall n m :
NZ,
n <
m ->
n ~=
m.
Theorem NZle_neq :
forall n m :
NZ,
n <
m <->
n <=
m /\
n ~=
m.
Theorem NZle_refl :
forall n :
NZ,
n <=
n.
Theorem NZlt_succ_diag_r :
forall n :
NZ,
n <
S n.
Theorem NZle_succ_diag_r :
forall n :
NZ,
n <=
S n.
Theorem NZlt_0_1 : 0 < 1.
Theorem NZle_0_1 : 0 <= 1.
Theorem NZlt_lt_succ_r :
forall n m :
NZ,
n <
m ->
n <
S m.
Theorem NZle_le_succ_r :
forall n m :
NZ,
n <=
m ->
n <=
S m.
Theorem NZle_succ_r :
forall n m :
NZ,
n <=
S m <->
n <=
m \/
n ==
S m.
Theorem NZneq_succ_diag_l :
forall n :
NZ,
S n ~=
n.
Theorem NZneq_succ_diag_r :
forall n :
NZ,
n ~=
S n.
Theorem NZnlt_succ_diag_l :
forall n :
NZ, ~
S n <
n.
Theorem NZnle_succ_diag_l :
forall n :
NZ, ~
S n <=
n.
Theorem NZle_succ_l :
forall n m :
NZ,
S n <=
m <->
n <
m.
Theorem NZlt_succ_l :
forall n m :
NZ,
S n <
m ->
n <
m.
Theorem NZsucc_lt_mono :
forall n m :
NZ,
n <
m <->
S n <
S m.
Theorem NZsucc_le_mono :
forall n m :
NZ,
n <=
m <->
S n <=
S m.
Theorem NZlt_asymm :
forall n m,
n <
m -> ~
m <
n.
Theorem NZlt_trans :
forall n m p :
NZ,
n <
m ->
m <
p ->
n <
p.
Theorem NZle_trans :
forall n m p :
NZ,
n <=
m ->
m <=
p ->
n <=
p.
Theorem NZle_lt_trans :
forall n m p :
NZ,
n <=
m ->
m <
p ->
n <
p.
Theorem NZlt_le_trans :
forall n m p :
NZ,
n <
m ->
m <=
p ->
n <
p.
Theorem NZle_antisymm :
forall n m :
NZ,
n <=
m ->
m <=
n ->
n ==
m.
Theorem NZlt_1_l :
forall n m :
NZ, 0 <
n ->
n <
m -> 1 <
m.
Trichotomy, decidability, and double negation elimination
Theorem NZlt_trichotomy :
forall n m :
NZ,
n <
m \/
n ==
m \/
m <
n.
Theorem NZeq_dec :
forall n m :
NZ,
decidable (
n ==
m).
Theorem NZeq_dne :
forall n m, ~ ~
n ==
m <->
n ==
m.
Theorem NZlt_gt_cases :
forall n m :
NZ,
n ~=
m <->
n <
m \/
n >
m.
Theorem NZle_gt_cases :
forall n m :
NZ,
n <=
m \/
n >
m.
Theorem NZlt_ge_cases :
forall n m :
NZ,
n <
m \/
n >=
m.
Theorem NZle_ge_cases :
forall n m :
NZ,
n <=
m \/
n >=
m.
Theorem NZle_ngt :
forall n m :
NZ,
n <=
m <-> ~
n >
m.
Theorem NZnlt_ge :
forall n m :
NZ, ~
n <
m <->
n >=
m.
Theorem NZlt_dec :
forall n m :
NZ,
decidable (
n <
m).
Theorem NZlt_dne :
forall n m, ~ ~
n <
m <->
n <
m.
Theorem NZnle_gt :
forall n m :
NZ, ~
n <=
m <->
n >
m.
Theorem NZlt_nge :
forall n m :
NZ,
n <
m <-> ~
n >=
m.
Theorem NZle_dec :
forall n m :
NZ,
decidable (
n <=
m).
Theorem NZle_dne :
forall n m :
NZ, ~ ~
n <=
m <->
n <=
m.
Theorem NZnlt_succ_r :
forall n m :
NZ, ~
m <
S n <->
n <
m.
Lemma NZlt_exists_pred_strong :
forall z n m :
NZ,
z <
m ->
m <=
n ->
exists k :
NZ,
m ==
S k /\
z <=
k.
Theorem NZlt_exists_pred :
forall z n :
NZ,
z <
n ->
exists k :
NZ,
n ==
S k /\
z <=
k.
A corollary of having an order is that NZ is infinite
Stronger variant of induction with assumptions n >= 0 (n < 0)
in the induction step
Section Induction.
Variable A :
NZ ->
Prop.
Hypothesis A_wd :
predicate_wd NZeq A.
Add Morphism A with signature NZeq ==>
iff as A_morph.
Section Center.
Variable z :
NZ.
Section RightInduction.
Let A' (
n :
NZ) :=
forall m :
NZ,
z <=
m ->
m <
n ->
A m.
Let right_step :=
forall n :
NZ,
z <=
n ->
A n ->
A (
S n).
Let right_step' :=
forall n :
NZ,
z <=
n ->
A' n ->
A n.
Let right_step'' :=
forall n :
NZ,
A' n <->
A' (
S n).
Lemma NZrs_rs' :
A z ->
right_step ->
right_step'.
Lemma NZrs'_rs'' :
right_step' ->
right_step''.
Lemma NZrbase :
A' z.
Lemma NZA'A_right : (
forall n :
NZ,
A' n) ->
forall n :
NZ,
z <=
n ->
A n.
Theorem NZstrong_right_induction:
right_step' ->
forall n :
NZ,
z <=
n ->
A n.
Theorem NZright_induction :
A z ->
right_step ->
forall n :
NZ,
z <=
n ->
A n.
Theorem NZright_induction' :
(
forall n :
NZ,
n <=
z ->
A n) ->
right_step ->
forall n :
NZ,
A n.
Theorem NZstrong_right_induction' :
(
forall n :
NZ,
n <=
z ->
A n) ->
right_step' ->
forall n :
NZ,
A n.
End RightInduction.
Section LeftInduction.
Let A' (
n :
NZ) :=
forall m :
NZ,
m <=
z ->
n <=
m ->
A m.
Let left_step :=
forall n :
NZ,
n <
z ->
A (
S n) ->
A n.
Let left_step' :=
forall n :
NZ,
n <=
z ->
A' (
S n) ->
A n.
Let left_step'' :=
forall n :
NZ,
A' n <->
A' (
S n).
Lemma NZls_ls' :
A z ->
left_step ->
left_step'.
Lemma NZls'_ls'' :
left_step' ->
left_step''.
Lemma NZlbase :
A' (
S z).
Lemma NZA'A_left : (
forall n :
NZ,
A' n) ->
forall n :
NZ,
n <=
z ->
A n.
Theorem NZstrong_left_induction:
left_step' ->
forall n :
NZ,
n <=
z ->
A n.
Theorem NZleft_induction :
A z ->
left_step ->
forall n :
NZ,
n <=
z ->
A n.
Theorem NZleft_induction' :
(
forall n :
NZ,
z <=
n ->
A n) ->
left_step ->
forall n :
NZ,
A n.
Theorem NZstrong_left_induction' :
(
forall n :
NZ,
z <=
n ->
A n) ->
left_step' ->
forall n :
NZ,
A n.
End LeftInduction.
Theorem NZorder_induction :
A z ->
(
forall n :
NZ,
z <=
n ->
A n ->
A (
S n)) ->
(
forall n :
NZ,
n <
z ->
A (
S n) ->
A n) ->
forall n :
NZ,
A n.
Theorem NZorder_induction' :
A z ->
(
forall n :
NZ,
z <=
n ->
A n ->
A (
S n)) ->
(
forall n :
NZ,
n <=
z ->
A n ->
A (
P n)) ->
forall n :
NZ,
A n.
End Center.
Theorem NZorder_induction_0 :
A 0 ->
(
forall n :
NZ, 0 <=
n ->
A n ->
A (
S n)) ->
(
forall n :
NZ,
n < 0 ->
A (
S n) ->
A n) ->
forall n :
NZ,
A n.
Theorem NZorder_induction'_0 :
A 0 ->
(
forall n :
NZ, 0 <=
n ->
A n ->
A (
S n)) ->
(
forall n :
NZ,
n <= 0 ->
A n ->
A (
P n)) ->
forall n :
NZ,
A n.
Elimintation principle for <
Theorem NZlt_ind :
forall (
n :
NZ),
A (
S n) ->
(
forall m :
NZ,
n <
m ->
A m ->
A (
S m)) ->
forall m :
NZ,
n <
m ->
A m.
Elimintation principle for <=