1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
From Stdlib 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.
Proof.
intro; apply lt_gt_cases.
Qed.
Theorem nonpos_pos_cases : forall n, n <= 0 \/ n > 0.
Proof.
intro; apply le_gt_cases.
Qed.
Theorem neg_nonneg_cases : forall n, n < 0 \/ n >= 0.
Proof.
intro; apply lt_ge_cases.
Qed.
Theorem nonpos_nonneg_cases : forall n, n <= 0 \/ n >= 0.
Proof.
intro; apply le_ge_cases.
Qed.
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.
Proof.
intro n; rewrite <- (succ_pred n) at 2; apply lt_succ_diag_r.
Qed.
Theorem le_pred_l : forall n, P n <= n.
Proof.
intro; apply lt_le_incl; apply lt_pred_l.
Qed.
Theorem lt_le_pred : forall n m, n < m <-> n <= P m.
Proof.
intros n m; rewrite <- (succ_pred m); rewrite pred_succ. apply lt_succ_r.
Qed.
Theorem nle_pred_r : forall n, ~ n <= P n.
Proof.
intro; rewrite <- lt_le_pred; apply lt_irrefl.
Qed.
Theorem lt_pred_le : forall n m, P n < m <-> n <= m.
Proof.
intros n m; rewrite <- (succ_pred n) at 2.
symmetry; apply le_succ_l.
Qed.
Theorem lt_lt_pred : forall n m, n < m -> P n < m.
Proof.
intros; apply lt_pred_le; now apply lt_le_incl.
Qed.
Theorem le_le_pred : forall n m, n <= m -> P n <= m.
Proof.
intros; apply lt_le_incl; now apply lt_pred_le.
Qed.
Theorem lt_pred_lt : forall n m, n < P m -> n < m.
Proof.
intros n m H; apply lt_trans with (P m); [assumption | apply lt_pred_l].
Qed.
Theorem le_pred_lt : forall n m, n <= P m -> n <= m.
Proof.
intros; apply lt_le_incl; now apply lt_le_pred.
Qed.
Theorem pred_lt_mono : forall n m, n < m <-> P n < P m.
Proof.
intros; rewrite lt_le_pred; symmetry; apply lt_pred_le.
Qed.
Theorem pred_le_mono : forall n m, n <= m <-> P n <= P m.
Proof.
intros; rewrite <- lt_pred_le; now rewrite lt_le_pred.
Qed.
Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m.
Proof.
intros n m; now rewrite (pred_lt_mono (S n) m), pred_succ.
Qed.
Theorem le_succ_le_pred : forall n m, S n <= m <-> n <= P m.
Proof.
intros n m; now rewrite (pred_le_mono (S n) m), pred_succ.
Qed.
Theorem lt_pred_lt_succ : forall n m, P n < m <-> n < S m.
Proof.
intros; rewrite lt_pred_le; symmetry; apply lt_succ_r.
Qed.
Theorem le_pred_lt_succ : forall n m, P n <= m <-> n <= S m.
Proof.
intros n m; now rewrite (pred_le_mono n (S m)), pred_succ.
Qed.
Theorem neq_pred_l : forall n, P n ~= n.
Proof.
intro; apply lt_neq; apply lt_pred_l.
Qed.
Theorem lt_m1_r : forall n m, n < m -> m < 0 -> n < -1.
Proof.
intros n m H1 H2. apply lt_le_pred in H2.
setoid_replace (P 0) with (-1) in H2.
- now apply lt_le_trans with m.
- apply eq_opp_r. now rewrite one_succ, opp_pred, opp_0.
Qed.
End ZOrderProp.
|
