Library Coq.Numbers.Natural.Abstract.NOrder
Require Export NMul.
Module NOrderPropFunct (
Import NAxiomsMod :
NAxiomsSig).
Module Export NMulPropMod :=
NMulPropFunct NAxiomsMod.
Open Local Scope NatScope.
Theorem lt_wd :
forall n1 n2 :
N,
n1 ==
n2 ->
forall m1 m2 :
N,
m1 ==
m2 -> (
n1 <
m1 <->
n2 <
m2).
Theorem le_wd :
forall n1 n2 :
N,
n1 ==
n2 ->
forall m1 m2 :
N,
m1 ==
m2 -> (
n1 <=
m1 <->
n2 <=
m2).
Theorem min_wd :
forall n1 n2 :
N,
n1 ==
n2 ->
forall m1 m2 :
N,
m1 ==
m2 ->
min n1 m1 ==
min n2 m2.
Theorem max_wd :
forall n1 n2 :
N,
n1 ==
n2 ->
forall m1 m2 :
N,
m1 ==
m2 ->
max n1 m1 ==
max n2 m2.
Theorem lt_eq_cases :
forall n m :
N,
n <=
m <->
n <
m \/
n ==
m.
Theorem lt_irrefl :
forall n :
N, ~
n <
n.
Theorem lt_succ_r :
forall n m :
N,
n <
S m <->
n <=
m.
Theorem min_l :
forall n m :
N,
n <=
m ->
min n m ==
n.
Theorem min_r :
forall n m :
N,
m <=
n ->
min n m ==
m.
Theorem max_l :
forall n m :
N,
m <=
n ->
max n m ==
n.
Theorem max_r :
forall n m :
N,
n <=
m ->
max n m ==
m.
Theorem lt_le_incl :
forall n m :
N,
n <
m ->
n <=
m.
Theorem eq_le_incl :
forall n m :
N,
n ==
m ->
n <=
m.
Theorem lt_neq :
forall n m :
N,
n <
m ->
n ~=
m.
Theorem le_neq :
forall n m :
N,
n <
m <->
n <=
m /\
n ~=
m.
Theorem le_refl :
forall n :
N,
n <=
n.
Theorem lt_succ_diag_r :
forall n :
N,
n <
S n.
Theorem le_succ_diag_r :
forall n :
N,
n <=
S n.
Theorem lt_0_1 : 0 < 1.
Theorem le_0_1 : 0 <= 1.
Theorem lt_lt_succ_r :
forall n m :
N,
n <
m ->
n <
S m.
Theorem le_le_succ_r :
forall n m :
N,
n <=
m ->
n <=
S m.
Theorem le_succ_r :
forall n m :
N,
n <=
S m <->
n <=
m \/
n ==
S m.
Theorem neq_succ_diag_l :
forall n :
N,
S n ~=
n.
Theorem neq_succ_diag_r :
forall n :
N,
n ~=
S n.
Theorem nlt_succ_diag_l :
forall n :
N, ~
S n <
n.
Theorem nle_succ_diag_l :
forall n :
N, ~
S n <=
n.
Theorem le_succ_l :
forall n m :
N,
S n <=
m <->
n <
m.
Theorem lt_succ_l :
forall n m :
N,
S n <
m ->
n <
m.
Theorem succ_lt_mono :
forall n m :
N,
n <
m <->
S n <
S m.
Theorem succ_le_mono :
forall n m :
N,
n <=
m <->
S n <=
S m.
Theorem lt_asymm :
forall n m :
N,
n <
m -> ~
m <
n.
Notation lt_ngt :=
lt_asymm (
only parsing).
Theorem lt_trans :
forall n m p :
N,
n <
m ->
m <
p ->
n <
p.
Theorem le_trans :
forall n m p :
N,
n <=
m ->
m <=
p ->
n <=
p.
Theorem le_lt_trans :
forall n m p :
N,
n <=
m ->
m <
p ->
n <
p.
Theorem lt_le_trans :
forall n m p :
N,
n <
m ->
m <=
p ->
n <
p.
Theorem le_antisymm :
forall n m :
N,
n <=
m ->
m <=
n ->
n ==
m.
Trichotomy, decidability, and double negation elimination
Theorem lt_trichotomy :
forall n m :
N,
n <
m \/
n ==
m \/
m <
n.
Notation lt_eq_gt_cases :=
lt_trichotomy (
only parsing).
Theorem lt_gt_cases :
forall n m :
N,
n ~=
m <->
n <
m \/
n >
m.
Theorem le_gt_cases :
forall n m :
N,
n <=
m \/
n >
m.
Theorem lt_ge_cases :
forall n m :
N,
n <
m \/
n >=
m.
Theorem le_ge_cases :
forall n m :
N,
n <=
m \/
n >=
m.
Theorem le_ngt :
forall n m :
N,
n <=
m <-> ~
n >
m.
Theorem nlt_ge :
forall n m :
N, ~
n <
m <->
n >=
m.
Theorem lt_dec :
forall n m :
N,
decidable (
n <
m).
Theorem lt_dne :
forall n m :
N, ~ ~
n <
m <->
n <
m.
Theorem nle_gt :
forall n m :
N, ~
n <=
m <->
n >
m.
Theorem lt_nge :
forall n m :
N,
n <
m <-> ~
n >=
m.
Theorem le_dec :
forall n m :
N,
decidable (
n <=
m).
Theorem le_dne :
forall n m :
N, ~ ~
n <=
m <->
n <=
m.
Theorem nlt_succ_r :
forall n m :
N, ~
m <
S n <->
n <
m.
Theorem lt_exists_pred :
forall z n :
N,
z <
n ->
exists k :
N,
n ==
S k /\
z <=
k.
Theorem lt_succ_iter_r :
forall (
n :
nat) (
m :
N),
m <
NZsucc_iter (
Datatypes.S n)
m.
Theorem neq_succ_iter_l :
forall (
n :
nat) (
m :
N),
NZsucc_iter (
Datatypes.S n)
m ~=
m.
Stronger variant of induction with assumptions n >= 0 (n < 0)
in the induction step
Theorem right_induction :
forall A :
N ->
Prop,
predicate_wd Neq A ->
forall z :
N,
A z ->
(
forall n :
N,
z <=
n ->
A n ->
A (
S n)) ->
forall n :
N,
z <=
n ->
A n.
Theorem left_induction :
forall A :
N ->
Prop,
predicate_wd Neq A ->
forall z :
N,
A z ->
(
forall n :
N,
n <
z ->
A (
S n) ->
A n) ->
forall n :
N,
n <=
z ->
A n.
Theorem right_induction' :
forall A :
N ->
Prop,
predicate_wd Neq A ->
forall z :
N,
(
forall n :
N,
n <=
z ->
A n) ->
(
forall n :
N,
z <=
n ->
A n ->
A (
S n)) ->
forall n :
N,
A n.
Theorem left_induction' :
forall A :
N ->
Prop,
predicate_wd Neq A ->
forall z :
N,
(
forall n :
N,
z <=
n ->
A n) ->
(
forall n :
N,
n <
z ->
A (
S n) ->
A n) ->
forall n :
N,
A n.
Theorem strong_right_induction :
forall A :
N ->
Prop,
predicate_wd Neq A ->
forall z :
N,
(
forall n :
N,
z <=
n -> (
forall m :
N,
z <=
m ->
m <
n ->
A m) ->
A n) ->
forall n :
N,
z <=
n ->
A n.
Theorem strong_left_induction :
forall A :
N ->
Prop,
predicate_wd Neq A ->
forall z :
N,
(
forall n :
N,
n <=
z -> (
forall m :
N,
m <=
z ->
S n <=
m ->
A m) ->
A n) ->
forall n :
N,
n <=
z ->
A n.
Theorem strong_right_induction' :
forall A :
N ->
Prop,
predicate_wd Neq A ->
forall z :
N,
(
forall n :
N,
n <=
z ->
A n) ->
(
forall n :
N,
z <=
n -> (
forall m :
N,
z <=
m ->
m <
n ->
A m) ->
A n) ->
forall n :
N,
A n.
Theorem strong_left_induction' :
forall A :
N ->
Prop,
predicate_wd Neq A ->
forall z :
N,
(
forall n :
N,
z <=
n ->
A n) ->
(
forall n :
N,
n <=
z -> (
forall m :
N,
m <=
z ->
S n <=
m ->
A m) ->
A n) ->
forall n :
N,
A n.
Theorem order_induction :
forall A :
N ->
Prop,
predicate_wd Neq A ->
forall z :
N,
A z ->
(
forall n :
N,
z <=
n ->
A n ->
A (
S n)) ->
(
forall n :
N,
n <
z ->
A (
S n) ->
A n) ->
forall n :
N,
A n.
Theorem order_induction' :
forall A :
N ->
Prop,
predicate_wd Neq A ->
forall z :
N,
A z ->
(
forall n :
N,
z <=
n ->
A n ->
A (
S n)) ->
(
forall n :
N,
n <=
z ->
A n ->
A (
P n)) ->
forall n :
N,
A n.
Elimintation principle for <
Theorem lt_ind :
forall A :
N ->
Prop,
predicate_wd Neq A ->
forall n :
N,
A (
S n) ->
(
forall m :
N,
n <
m ->
A m ->
A (
S m)) ->
forall m :
N,
n <
m ->
A m.
Elimintation principle for <=
Theorem le_ind :
forall A :
N ->
Prop,
predicate_wd Neq A ->
forall n :
N,
A n ->
(
forall m :
N,
n <=
m ->
A m ->
A (
S m)) ->
forall m :
N,
n <=
m ->
A m.
Well-founded relations
Theorem lt_wf :
forall z :
N,
well_founded (
fun n m :
N =>
z <=
n /\
n <
m).
Theorem gt_wf :
forall z :
N,
well_founded (
fun n m :
N =>
m <
n /\
n <=
z).
Theorem lt_wf_0 :
well_founded lt.
Theorem nlt_0_r :
forall n :
N, ~
n < 0.
Theorem nle_succ_0 :
forall n :
N, ~ (
S n <= 0).
Theorem le_0_r :
forall n :
N,
n <= 0 <->
n == 0.
Theorem lt_0_succ :
forall n :
N, 0 <
S n.
Theorem neq_0_lt_0 :
forall n :
N,
n ~= 0 <-> 0 <
n.
Theorem eq_0_gt_0_cases :
forall n :
N,
n == 0 \/ 0 <
n.
Theorem zero_one :
forall n :
N,
n == 0 \/
n == 1 \/ 1 <
n.
Theorem lt_1_r :
forall n :
N,
n < 1 <->
n == 0.
Theorem le_1_r :
forall n :
N,
n <= 1 <->
n == 0 \/
n == 1.
Theorem lt_lt_0 :
forall n m :
N,
n <
m -> 0 <
m.
Theorem lt_1_l :
forall n m p :
N,
n <
m ->
m <
p -> 1 <
p.
Elimination principlies for < and <= for relations
Section RelElim.
Variable R :
N ->
N ->
Prop.
Hypothesis R_wd :
relation_wd Neq Neq R.
Add Morphism R with signature Neq ==>
Neq ==>
iff as R_morph2.
Theorem le_ind_rel :
(
forall m :
N,
R 0
m) ->
(
forall n m :
N,
n <=
m ->
R n m ->
R (
S n) (
S m)) ->
forall n m :
N,
n <=
m ->
R n m.
Theorem lt_ind_rel :
(
forall m :
N,
R 0 (
S m)) ->
(
forall n m :
N,
n <
m ->
R n m ->
R (
S n) (
S m)) ->
forall n m :
N,
n <
m ->
R n m.
End RelElim.
Predecessor and order
Theorem succ_pred_pos :
forall n :
N, 0 <
n ->
S (
P n) ==
n.
Theorem le_pred_l :
forall n :
N,
P n <=
n.
Theorem lt_pred_l :
forall n :
N,
n ~= 0 ->
P n <
n.
Theorem le_le_pred :
forall n m :
N,
n <=
m ->
P n <=
m.
Theorem lt_lt_pred :
forall n m :
N,
n <
m ->
P n <
m.
Theorem lt_le_pred :
forall n m :
N,
n <
m ->
n <=
P m.
Theorem lt_pred_le :
forall n m :
N,
P n <
m ->
n <=
m.
Theorem lt_pred_lt :
forall n m :
N,
n <
P m ->
n <
m.
Theorem le_pred_le :
forall n m :
N,
n <=
P m ->
n <=
m.
Theorem pred_le_mono :
forall n m :
N,
n <=
m ->
P n <=
P m.
Theorem pred_lt_mono :
forall n m :
N,
n ~= 0 -> (
n <
m <->
P n <
P m).
Theorem lt_succ_lt_pred :
forall n m :
N,
S n <
m <->
n <
P m.
Theorem le_succ_le_pred :
forall n m :
N,
S n <=
m ->
n <=
P m.
Theorem lt_pred_lt_succ :
forall n m :
N,
P n <
m ->
n <
S m.
Theorem le_pred_le_succ :
forall n m :
N,
P n <=
m <->
n <=
S m.
End NOrderPropFunct.