]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground_1/blt/props.ma
frees_drops, initial versrion
[helm.git] / matita / matita / contribs / lambdadelta / ground_1 / blt / props.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 (* This file was automatically generated: do not edit *********************)
16
17 include "ground_1/blt/defs.ma".
18
19 lemma lt_blt:
20  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq bool (blt y x) true)))
21 \def
22  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to 
23 (eq bool (blt y n) true)))) (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0 
24 \def (match H with [le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let H1 
25 \def (eq_ind nat (S y) (\lambda (e: nat).(match e with [O \Rightarrow False | 
26 (S _) \Rightarrow True])) I O H0) in (False_ind (eq bool (blt y O) true) 
27 H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def 
28 (eq_ind nat (S m) (\lambda (e: nat).(match e with [O \Rightarrow False | (S 
29 _) \Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq bool (blt 
30 y O) true)) H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda (n: 
31 nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq bool (blt y n) 
32 true))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0 (S n)) \to 
33 (eq bool (blt n0 (S n)) true))) (\lambda (_: (lt O (S n))).(refl_equal bool 
34 true)) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n)) \to (eq bool (match n0 
35 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true)))).(\lambda 
36 (H1: (lt (S n0) (S n))).(H n0 (le_S_n (S n0) n H1))))) y)))) x).
37
38 lemma le_bge:
39  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq bool (blt y x) false)))
40 \def
41  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to 
42 (eq bool (blt y n) false)))) (\lambda (y: nat).(\lambda (_: (le O 
43 y)).(refl_equal bool false))) (\lambda (n: nat).(\lambda (H: ((\forall (y: 
44 nat).((le n y) \to (eq bool (blt y n) false))))).(\lambda (y: nat).(nat_ind 
45 (\lambda (n0: nat).((le (S n) n0) \to (eq bool (blt n0 (S n)) false))) 
46 (\lambda (H0: (le (S n) O)).(let H1 \def (match H0 with [le_n \Rightarrow 
47 (\lambda (H1: (eq nat (S n) O)).(let H2 \def (eq_ind nat (S n) (\lambda (e: 
48 nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) 
49 in (False_ind (eq bool (blt O (S n)) false) H2))) | (le_S m H1) \Rightarrow 
50 (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: 
51 nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) 
52 in (False_ind ((le (S n) m) \to (eq bool (blt O (S n)) false)) H3)) H1))]) in 
53 (H1 (refl_equal nat O)))) (\lambda (n0: nat).(\lambda (_: (((le (S n) n0) \to 
54 (eq bool (blt n0 (S n)) false)))).(\lambda (H1: (le (S n) (S n0))).(H n0 
55 (le_S_n n n0 H1))))) y)))) x).
56
57 lemma blt_lt:
58  \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) true) \to (lt y x)))
59 \def
60  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt 
61 y n) true) \to (lt y n)))) (\lambda (y: nat).(\lambda (H: (eq bool (blt y O) 
62 true)).(let H0 \def (match H with [refl_equal \Rightarrow (\lambda (H0: (eq 
63 bool (blt y O) true)).(let H1 \def (eq_ind bool (blt y O) (\lambda (e: 
64 bool).(match e with [true \Rightarrow False | false \Rightarrow True])) I 
65 true H0) in (False_ind (lt y O) H1)))]) in (H0 (refl_equal bool true))))) 
66 (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq bool (blt y n) true) 
67 \to (lt y n))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((eq bool (blt 
68 n0 (S n)) true) \to (lt n0 (S n)))) (\lambda (_: (eq bool true true)).(le_S_n 
69 (S O) (S n) (le_n_S (S O) (S n) (le_n_S O n (le_O_n n))))) (\lambda (n0: 
70 nat).(\lambda (_: (((eq bool (match n0 with [O \Rightarrow true | (S m) 
71 \Rightarrow (blt m n)]) true) \to (lt n0 (S n))))).(\lambda (H1: (eq bool 
72 (blt n0 n) true)).(lt_n_S n0 n (H n0 H1))))) y)))) x).
73
74 lemma bge_le:
75  \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) false) \to (le x y)))
76 \def
77  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt 
78 y n) false) \to (le n y)))) (\lambda (y: nat).(\lambda (_: (eq bool (blt y O) 
79 false)).(le_O_n y))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq 
80 bool (blt y n) false) \to (le n y))))).(\lambda (y: nat).(nat_ind (\lambda 
81 (n0: nat).((eq bool (blt n0 (S n)) false) \to (le (S n) n0))) (\lambda (H0: 
82 (eq bool (blt O (S n)) false)).(let H1 \def (match H0 with [refl_equal 
83 \Rightarrow (\lambda (H1: (eq bool (blt O (S n)) false)).(let H2 \def (eq_ind 
84 bool (blt O (S n)) (\lambda (e: bool).(match e with [true \Rightarrow True | 
85 false \Rightarrow False])) I false H1) in (False_ind (le (S n) O) H2)))]) in 
86 (H1 (refl_equal bool false)))) (\lambda (n0: nat).(\lambda (_: (((eq bool 
87 (blt n0 (S n)) false) \to (le (S n) n0)))).(\lambda (H1: (eq bool (blt (S n0) 
88 (S n)) false)).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S n n0 (H n0 
89 H1))))))) y)))) x).
90