blob: 6368fa5578eb1f805df73a8df89df6e974c8cb5c (
plain)
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
|
Require Export NZPlus.
Require Export NZOrder.
Module NZPlusOrderPropFunct
(Import NZPlusMod : NZPlusSig)
(Import NZOrderMod : NZOrderSig with Module NZBaseMod := NZPlusMod.NZBaseMod).
Module Export NZPlusPropMod := NZPlusPropFunct NZPlusMod.
Module Export NZOrderPropMod := NZOrderPropFunct NZOrderMod.
Open Local Scope NatIntScope.
Theorem NZplus_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
Proof.
intros n m p; NZinduct p.
now do 2 rewrite NZplus_0_l.
intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_lt_mono.
Qed.
Theorem NZplus_lt_mono_r : forall n m p, n < m <-> n + p < m + p.
Proof.
intros n m p.
rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_lt_mono_l.
Qed.
Theorem NZplus_lt_mono : forall n m p q, n < m -> p < q -> n + p < m + q.
Proof.
intros n m p q H1 H2.
apply NZlt_trans with (m + p);
[now apply -> NZplus_lt_mono_r | now apply -> NZplus_lt_mono_l].
Qed.
Theorem NZplus_le_mono_l : forall n m p, n <= m <-> p + n <= p + m.
Proof.
intros n m p; NZinduct p.
now do 2 rewrite NZplus_0_l.
intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_le_mono.
Qed.
Theorem NZplus_le_mono_r : forall n m p, n <= m <-> n + p <= m + p.
Proof.
intros n m p.
rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_le_mono_l.
Qed.
Theorem NZplus_le_mono : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
Proof.
intros n m p q H1 H2.
apply NZle_trans with (m + p);
[now apply -> NZplus_le_mono_r | now apply -> NZplus_le_mono_l].
Qed.
Theorem NZplus_lt_le_mono : forall n m p q, n < m -> p <= q -> n + p < m + q.
Proof.
intros n m p q H1 H2.
apply NZlt_le_trans with (m + p);
[now apply -> NZplus_lt_mono_r | now apply -> NZplus_le_mono_l].
Qed.
Theorem NZplus_le_lt_mono : forall n m p q, n <= m -> p < q -> n + p < m + q.
Proof.
intros n m p q H1 H2.
apply NZle_lt_trans with (m + p);
[now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l].
Qed.
End NZPlusOrderPropFunct.
|
