1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/library_autobatch/Z/orders".
17 include "auto/Z/z.ma".
18 include "auto/nat/orders.ma".
20 definition Zle : Z \to Z \to Prop \def
26 | (pos m) \Rightarrow True
27 | (neg m) \Rightarrow False ]
30 [ OZ \Rightarrow False
31 | (pos m) \Rightarrow n \leq m
32 | (neg m) \Rightarrow False ]
36 | (pos m) \Rightarrow True
37 | (neg m) \Rightarrow m \leq n ]].
39 interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
40 interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
42 definition Zlt : Z \to Z \to Prop \def
47 [ OZ \Rightarrow False
48 | (pos m) \Rightarrow True
49 | (neg m) \Rightarrow False ]
52 [ OZ \Rightarrow False
53 | (pos m) \Rightarrow n<m
54 | (neg m) \Rightarrow False ]
58 | (pos m) \Rightarrow True
59 | (neg m) \Rightarrow m<n ]].
61 interpretation "integer 'less than'" 'lt x y = (Zlt x y).
62 interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
64 theorem irreflexive_Zlt: irreflexive Z Zlt.
69 [ (*qui autobatch non chiude il goal*)
71 | cut (neg n < neg n \to False)
73 (*qui autobatch non chiude il goal*)
80 | cut (pos n < pos n \to False)
82 (*qui autobatch non chiude il goal*)
92 theorem irrefl_Zlt: irreflexive Z Zlt
95 theorem Zlt_neg_neg_to_lt:
96 \forall n,m:nat. neg n < neg m \to m < n.
98 (*qui autobatch non chiude il goal*)
102 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.m < n \to neg n < neg m.
108 theorem Zlt_pos_pos_to_lt:
109 \forall n,m:nat. pos n < pos m \to n < m.
111 (*qui autobatch non chiude il goal*)
115 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.n < m \to pos n < pos m.
121 theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
125 cut (OZ < y \to Zsucc OZ \leq y)
132 (*qui autobatch non chiude il goal*)
137 (*qui autobatch non chiude il goal*)
144 cut (neg n < y \to Zsucc (neg n) \leq y)
149 [ cut (neg O < y \to Zsucc (neg O) \leq y)
160 (*qui autobatch non chiude il goal*)
161 apply (not_le_Sn_O n1 H2)
164 | cut (neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y)
175 (*qui autobatch non chiude il goal*)
176 apply (le_S_S_to_le n2 n1 H3)