1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/blt/props".
19 include "blt/defs.ma".
22 \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq bool (blt y x) true)))
24 \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to
25 (eq bool (blt y n) true)))) (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0
26 \def (match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat
27 n O) \to (eq bool (blt y O) true)))) with [le_n \Rightarrow (\lambda (H0: (eq
28 nat (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e in
29 nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
30 \Rightarrow True])) I O H0) in (False_ind (eq bool (blt y O) true) H1))) |
31 (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind
32 nat (S m) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop)
33 with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind
34 ((le (S y) m) \to (eq bool (blt y O) true)) H2)) H0))]) in (H0 (refl_equal
35 nat O))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to
36 (eq bool (blt y n) true))))).(\lambda (y: nat).(nat_ind (\lambda (n0:
37 nat).((lt n0 (S n)) \to (eq bool (blt n0 (S n)) true))) (\lambda (_: (lt O (S
38 n))).(refl_equal bool true)) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n))
39 \to (eq bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m
40 n)]) true)))).(\lambda (H1: (lt (S n0) (S n))).(H n0 (le_S_n (S n0) n H1)))))
44 \forall (x: nat).(\forall (y: nat).((le x y) \to (eq bool (blt y x) false)))
46 \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to
47 (eq bool (blt y n) false)))) (\lambda (y: nat).(\lambda (_: (le O
48 y)).(refl_equal bool false))) (\lambda (n: nat).(\lambda (H: ((\forall (y:
49 nat).((le n y) \to (eq bool (blt y n) false))))).(\lambda (y: nat).(nat_ind
50 (\lambda (n0: nat).((le (S n) n0) \to (eq bool (blt n0 (S n)) false)))
51 (\lambda (H0: (le (S n) O)).(let H1 \def (match H0 in le return (\lambda (n0:
52 nat).(\lambda (_: (le ? n0)).((eq nat n0 O) \to (eq bool (blt O (S n))
53 false)))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def
54 (eq_ind nat (S n) (\lambda (e: nat).(match e in nat return (\lambda (_:
55 nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in
56 (False_ind (eq bool (blt O (S n)) false) H2))) | (le_S m H1) \Rightarrow
57 (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e:
58 nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False
59 | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S n) m) \to (eq bool
60 (blt O (S n)) false)) H3)) H1))]) in (H1 (refl_equal nat O)))) (\lambda (n0:
61 nat).(\lambda (_: (((le (S n) n0) \to (eq bool (blt n0 (S n))
62 false)))).(\lambda (H1: (le (S n) (S n0))).(H n0 (le_S_n n n0 H1))))) y))))
66 \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) true) \to (lt y x)))
68 \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt
69 y n) true) \to (lt y n)))) (\lambda (y: nat).(\lambda (H: (eq bool (blt y O)
70 true)).(let H0 \def (match H in eq return (\lambda (b: bool).(\lambda (_: (eq
71 ? ? b)).((eq bool b true) \to (lt y O)))) with [refl_equal \Rightarrow
72 (\lambda (H0: (eq bool (blt y O) true)).(let H1 \def (eq_ind bool (blt y O)
73 (\lambda (e: bool).(match e in bool return (\lambda (_: bool).Prop) with
74 [true \Rightarrow False | false \Rightarrow True])) I true H0) in (False_ind
75 (lt y O) H1)))]) in (H0 (refl_equal bool true))))) (\lambda (n: nat).(\lambda
76 (H: ((\forall (y: nat).((eq bool (blt y n) true) \to (lt y n))))).(\lambda
77 (y: nat).(nat_ind (\lambda (n0: nat).((eq bool (blt n0 (S n)) true) \to (lt
78 n0 (S n)))) (\lambda (_: (eq bool true true)).(le_S_n (S O) (S n) (le_n_S (S
79 O) (S n) (le_n_S O n (le_O_n n))))) (\lambda (n0: nat).(\lambda (_: (((eq
80 bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true)
81 \to (lt n0 (S n))))).(\lambda (H1: (eq bool (blt n0 n) true)).(lt_le_S (S n0)
82 (S n) (lt_n_S n0 n (H n0 H1)))))) y)))) x).
85 \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) false) \to (le x y)))
87 \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt
88 y n) false) \to (le n y)))) (\lambda (y: nat).(\lambda (_: (eq bool (blt y O)
89 false)).(le_O_n y))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq
90 bool (blt y n) false) \to (le n y))))).(\lambda (y: nat).(nat_ind (\lambda
91 (n0: nat).((eq bool (blt n0 (S n)) false) \to (le (S n) n0))) (\lambda (H0:
92 (eq bool (blt O (S n)) false)).(let H1 \def (match H0 in eq return (\lambda
93 (b: bool).(\lambda (_: (eq ? ? b)).((eq bool b false) \to (le (S n) O))))
94 with [refl_equal \Rightarrow (\lambda (H1: (eq bool (blt O (S n))
95 false)).(let H2 \def (eq_ind bool (blt O (S n)) (\lambda (e: bool).(match e
96 in bool return (\lambda (_: bool).Prop) with [true \Rightarrow True | false
97 \Rightarrow False])) I false H1) in (False_ind (le (S n) O) H2)))]) in (H1
98 (refl_equal bool false)))) (\lambda (n0: nat).(\lambda (_: (((eq bool (blt n0
99 (S n)) false) \to (le (S n) n0)))).(\lambda (H1: (eq bool (blt (S n0) (S n))
100 false)).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S n n0 (H n0