]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_pred_succ.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / ynat_lt_pred_succ.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground/arith/ynat_succ.ma".
16 include "ground/arith/ynat_lt_pred.ma".
17
18 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
19
20 (* Constructions with ypred and ysucc ***************************************)
21
22 (*** ylt_O1 *)
23 lemma ylt_zero_sn (y): y = โ†‘โ†“y โ†’ ๐ŸŽ < y.
24 #y @(ynat_split_nat_inf โ€ฆ y) -y
25 /4 width=1 by ylt_inj, eq_inv_yinj_nat_bi, nlt_zero_sn/
26 qed.
27
28 (* Destructions with ypred and ysucc ****************************************)
29
30 (*** ylt_inv_O1 *)
31 lemma ylt_des_gen_dx (x) (y): x < y โ†’ y = โ†‘โ†“y.
32 #x #y * //
33 #m #n #H
34 lapply (nlt_des_gen โ€ฆ H) -H //
35 qed-.
36
37 lemma ylt_des_succ_sn (x) (y):
38       โ†‘x < y โ†’ x < โ†“y.
39 #x #y @(insert_eq_1 โ€ฆ (โ†‘x))
40 #x0 * -x0 -y
41 [ #m0 #n #Hn #H
42   elim (eq_inv_ysucc_inj โ€ฆ H) -H #m #H1 #H2 destruct
43   elim (nlt_inv_succ_sn โ€ฆ Hn) -Hn #Hm #_
44   /2 width=1 by ylt_inj/
45 | #m0 #H
46   elim (eq_inv_ysucc_inj โ€ฆ H) -H #m #H1 #H2 destruct //  
47 ]
48 qed-.
49
50 (* Inversions with ypred and ysucc ******************************************)
51
52 (*** ylt_inv_succ1 *)
53 lemma ylt_inv_succ_sn (x) (y):
54       โ†‘x < y โ†’ โˆงโˆง x < โ†“y & y = โ†‘โ†“y.
55 /3 width=2 by ylt_des_succ_sn, ylt_des_gen_dx, conj/ qed-.