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
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
Require Export ZOrder.
Require Export ZPlus.
Module PlusOrderProperties (PlusModule : PlusSignature)
(OrderModule : OrderSignature with
Module IntModule := PlusModule.IntModule).
(* Warning: Notation _ == _ was already used in scope ZScope !!! *)
Module Export PlusPropertiesModule := PlusProperties PlusModule.
Module Export OrderPropertiesModule := OrderProperties OrderModule.
(* <W> Grammar extension: in [tactic:simple_tactic], some rule has been masked !!! *)
Open Local Scope ZScope.
Theorem plus_lt_compat_l : forall n m p, n < m <-> p + n < p + m.
Proof.
intros n m p; induct p.
now do 2 rewrite plus_0.
intros p IH. do 2 rewrite plus_S. now rewrite <- lt_respects_S.
intros p IH. do 2 rewrite plus_P. now rewrite <- lt_respects_P.
Qed.
Theorem plus_lt_compat_r : forall n m p, n < m <-> n + p < m + p.
Proof.
intros n m p; rewrite (plus_comm n p); rewrite (plus_comm m p);
apply plus_lt_compat_l.
Qed.
Theorem plus_le_compat_l : forall n m p, n <= m <-> p + n <= p + m.
Proof.
intros n m p; do 2 rewrite <- lt_S. rewrite <- plus_n_Sm;
apply plus_lt_compat_l.
Qed.
Theorem plus_le_compat_r : forall n m p, n <= m <-> n + p <= m + p.
Proof.
intros n m p; rewrite (plus_comm n p); rewrite (plus_comm m p);
apply plus_le_compat_l.
Qed.
Theorem plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
Proof.
intros n m p q H1 H2. apply lt_trans with (m := m + p).
now apply -> plus_lt_compat_r. now apply -> plus_lt_compat_l.
Qed.
Theorem plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q.
Proof.
intros n m p q H1 H2. le_elim H2. now apply plus_lt_compat.
rewrite H2. now apply -> plus_lt_compat_r.
Qed.
Theorem plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q.
Proof.
intros n m p q H1 H2. le_elim H1. now apply plus_lt_compat.
rewrite H1. now apply -> plus_lt_compat_l.
Qed.
Theorem plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
Proof.
intros n m p q H1 H2. le_elim H1. le_intro1; now apply plus_lt_le_compat.
rewrite H1. now apply -> plus_le_compat_l.
Qed.
Theorem plus_pos : forall n m, 0 <= n -> 0 <= m -> 0 <= n + m.
Proof.
intros; rewrite <- (plus_0 0); now apply plus_le_compat.
Qed.
Lemma lt_opp_forward : forall n m, n < m -> - m < - n.
Proof.
induct n.
induct_ord m.
intro H; false_hyp H lt_irr.
intros m H1 IH H2. rewrite uminus_S. rewrite uminus_0 in *.
le_elim H1. apply IH in H1. now apply lt_Pn_m.
rewrite <- H1; rewrite uminus_0; apply lt_Pn_n.
intros m H1 IH H2. apply lt_n_Pm in H2. apply -> le_gt in H1. false_hyp H2 H1.
intros n IH m H. rewrite uminus_S.
apply -> lt_S_P in H. apply IH in H. rewrite uminus_P in H. now apply -> lt_S_P.
intros n IH m H. rewrite uminus_P.
apply -> lt_P_S in H. apply IH in H. rewrite uminus_S in H. now apply -> lt_P_S.
Qed.
Theorem lt_opp : forall n m, n < m <-> - m < - n.
Proof.
intros n m; split.
apply lt_opp_forward.
intro; rewrite <- (double_opp n); rewrite <- (double_opp m);
now apply lt_opp_forward.
Qed.
Theorem le_opp : forall n m, n <= m <-> - m <= - n.
Proof.
intros n m; do 2 rewrite -> le_lt; rewrite <- lt_opp.
assert (n == m <-> - m == - n).
split; intro; [now apply uminus_wd | now apply opp_inj].
tauto.
Qed.
Theorem lt_opp_neg : forall n, n < 0 <-> 0 < - n.
Proof.
intro n. set (k := 0) in |-* at 2.
setoid_replace k with (- k); unfold k; clear k.
apply lt_opp. now rewrite uminus_0.
Qed.
Theorem le_opp_neg : forall n, n <= 0 <-> 0 <= - n.
Proof.
intro n. set (k := 0) in |-* at 2.
setoid_replace k with (- k); unfold k; clear k.
apply le_opp. now rewrite uminus_0.
Qed.
Theorem lt_opp_pos : forall n, 0 < n <-> - n < 0.
Proof.
intro n. set (k := 0) in |-* at 2.
setoid_replace k with (- k); unfold k; clear k.
apply lt_opp. now rewrite uminus_0.
Qed.
Theorem le_opp_pos : forall n, 0 <= n <-> - n <= 0.
Proof.
intro n. set (k := 0) in |-* at 2.
setoid_replace k with (- k); unfold k; clear k.
apply le_opp. now rewrite uminus_0.
Qed.
Theorem minus_lt_decr_r : forall n m p, n < m <-> p - m < p - n.
Proof.
intros n m p. do 2 rewrite <- plus_opp_minus. rewrite <- plus_lt_compat_l.
apply lt_opp.
Qed.
Theorem minus_le_nonincr_r : forall n m p, n <= m <-> p - m <= p - n.
Proof.
intros n m p. do 2 rewrite <- plus_opp_minus. rewrite <- plus_le_compat_l.
apply le_opp.
Qed.
Theorem minus_lt_incr_l : forall n m p, n < m <-> n - p < m - p.
Proof.
intros n m p. do 2 rewrite <- plus_opp_minus. now rewrite <- plus_lt_compat_r.
Qed.
Theorem minus_le_nondecr_l : forall n m p, n <= m <-> n - p <= m - p.
Proof.
intros n m p. do 2 rewrite <- plus_opp_minus. now rewrite <- plus_le_compat_r.
Qed.
Theorem lt_plus_swap : forall n m p, n + p < m <-> n < m - p.
Proof.
intros n m p. rewrite (minus_lt_incr_l (n + p) m p).
rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0.
Qed.
Theorem le_plus_swap : forall n m p, n + p <= m <-> n <= m - p.
Proof.
intros n m p. rewrite (minus_le_nondecr_l (n + p) m p).
rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0.
Qed.
End PlusOrderProperties.
|
