2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/relations.ma".
14 inductive nat : Type[0] ≝
18 interpretation "Natural numbers" 'N = nat.
20 alias num (instance 0) = "natural number".
23 λn. match n with [ O ⇒
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 | S p ⇒ p].
25 theorem pred_Sn : ∀n.n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"
\ 6pred
\ 5/a
\ 6 (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n).
28 theorem injective_S :
\ 5a href="cic:/matita/basics/relations/injective.def(1)"
\ 6injective
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6.
32 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
35 theorem not_eq_S: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 m →
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m.
36 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
38 definition not_zero:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 → Prop ≝
39 λn:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. match n with [ O ⇒
\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"
\ 6False
\ 5/a
\ 6 | (S p) ⇒
\ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"
\ 6True
\ 5/a
\ 6 ].
41 theorem not_eq_O_S : ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n.
42 #n @
\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"
\ 6nmk
\ 5/a
\ 6 #eqOS (change with (
\ 5a href="cic:/matita/arithmetics/nat/not_zero.def(1)"
\ 6not_zero
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6)) >eqOS // qed.
44 theorem not_eq_n_Sn: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n.
45 #n (elim n) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"
\ 6not_eq_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
48 ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.∀P:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 → Prop.
49 (n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 → P
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6) → (∀m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m → P (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m)) → P n.
50 #n #P (elim n) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/ qed.
53 ∀R:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 → Prop.
54 (∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. R
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 n)
55 → (∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. R (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n)
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6)
56 → (∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. R n m → R (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n) (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m))
57 → ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. R n m.
58 #R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/ qed.
60 theorem decidable_eq_nat : ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/basics/logic/decidable.def(1)"
\ 6decidable
\ 5/a
\ 6 (n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6m).
61 @
\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"
\ 6nat_elim2
\ 5/a
\ 6 #n [ (cases n) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"
\ 6or_introl
\ 5/a
\ 6,
\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"
\ 6or_intror
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ | /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"
\ 6or_intror
\ 5/a
\ 6,
\ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"
\ 6sym_not_eq
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ | #m #Hind (cases Hind) /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"
\ 6or_introl
\ 5/a
\ 6,
\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"
\ 6or_intror
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"
\ 6not_eq_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/]
64 (*************************** plus ******************************)
67 match n with [ O ⇒ m | S p ⇒
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (plus p m) ].
69 interpretation "natural plus" 'plus x y = (plus x y).
71 theorem plus_O_n: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6n.
75 theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m.
79 theorem plus_n_O: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"
\ 60
\ 5/a
\ 6.
80 #n (elim n) normalize // qed.
82 theorem plus_n_Sm : ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6m)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m.
83 #n (elim n) normalize // qed.
86 theorem plus_Sn_m1: ∀n,m:nat. S m + n = n + S m.
87 #n (elim n) normalize // qed.
91 theorem plus_n_1 : ∀n:nat. S n = n+1.
95 theorem commutative_plus:
\ 5a href="cic:/matita/basics/relations/commutative.def(1)"
\ 6commutative
\ 5/a
\ 6 ?
\ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"
\ 6plus
\ 5/a
\ 6.
96 #n (elim n) normalize // qed.
98 theorem associative_plus :
\ 5a href="cic:/matita/basics/relations/associative.def(1)"
\ 6associative
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"
\ 6plus
\ 5/a
\ 6.
99 #n (elim n) normalize // qed.
101 theorem assoc_plus1: ∀a,b,c. c
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 (b
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 a)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 b
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 c
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 a.
104 theorem injective_plus_r: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/basics/relations/injective.def(1)"
\ 6injective
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 (λm.n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6m).
105 #n (elim n) normalize /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"
\ 6injective_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
107 (* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
108 \def injective_plus_r.
110 theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m).
113 (* theorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m
114 \def injective_plus_l. *)
116 (*************************** times *****************************)
119 match n with [ O ⇒
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 | S p ⇒ m
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6(times p m) ].
121 interpretation "natural times" 'times x y = (times x y).
123 theorem times_Sn_m: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. m
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6m.
126 theorem times_O_n: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6n.
129 theorem times_n_O: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6.
132 theorem times_n_Sm : ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6(n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6m)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6(
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m).
133 #n (elim n) normalize // qed.
135 theorem commutative_times :
\ 5a href="cic:/matita/basics/relations/commutative.def(1)"
\ 6commutative
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"
\ 6times
\ 5/a
\ 6.
136 #n (elim n) normalize // qed.
138 (* variant sym_times : \forall n,m:nat. n*m = m*n \def
141 theorem distributive_times_plus :
\ 5a href="cic:/matita/basics/relations/distributive.def(1)"
\ 6distributive
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"
\ 6times
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"
\ 6plus
\ 5/a
\ 6.
142 #n (elim n) normalize // qed.
144 theorem distributive_times_plus_r :
145 ∀a,b,c:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. (b
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6c)
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 b
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6a
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 c
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6a.
148 theorem associative_times:
\ 5a href="cic:/matita/basics/relations/associative.def(1)"
\ 6associative
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"
\ 6times
\ 5/a
\ 6.
149 #n (elim n) normalize // qed.
151 lemma times_times: ∀x,y,z. x
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6(y
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6z)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 y
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6(x
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6z).
154 theorem times_n_1 : ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"
\ 61
\ 5/a
\ 6.
157 (* ci servono questi risultati?
158 theorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
160 #n #m #H normalize #H1 napply False_ind napply not_eq_O_S
163 theorem times_n_SO : ∀n:nat. n = n * S O.
166 theorem times_SSO_n : ∀n:nat. n + n = (S(S O)) * n.
169 nlemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
172 theorem or_eq_eq_S: \forall n.\exists m.
173 n = (S(S O))*m \lor n = S ((S(S O))*m).
176 ##|#a #H nelim H #b#ornelim or#aeq
183 (******************** ordering relations ************************)
185 inductive le (n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6) :
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 → Prop ≝
187 | le_S : ∀ m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. le n m → le n (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m).
189 interpretation "natural 'less or equal to'" 'leq x y = (le x y).
191 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
193 definition lt:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 → Prop ≝ λn,m.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m.
195 interpretation "natural 'less than'" 'lt x y = (lt x y).
196 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
198 (* lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m).
201 definition ge:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 → Prop ≝ λn,m.m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n.
203 interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
205 definition gt:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 → Prop ≝ λn,m.m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6n.
207 interpretation "natural 'greater than'" 'gt x y = (gt x y).
208 interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
210 theorem transitive_le :
\ 5a href="cic:/matita/basics/relations/transitive.def(2)"
\ 6transitive
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"
\ 6le
\ 5/a
\ 6.
211 #a #b #c #leab #lebc (elim lebc) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"
\ 6le_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
215 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
216 \def transitive_le. *)
218 theorem transitive_lt:
\ 5a href="cic:/matita/basics/relations/transitive.def(2)"
\ 6transitive
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"
\ 6lt
\ 5/a
\ 6.
219 #a #b #c #ltab #ltbc (elim ltbc) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"
\ 6le_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/qed.
222 theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
223 \def transitive_lt. *)
225 theorem le_S_S: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m →
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m.
226 #n #m #lenm (elim lenm) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"
\ 6le_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
228 theorem le_O_n : ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n.
229 #n (elim n) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"
\ 6le_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
231 theorem le_n_Sn : ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n.
232 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"
\ 6le_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
234 theorem le_pred_n : ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"
\ 6pred
\ 5/a
\ 6 n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n.
237 theorem monotonic_pred:
\ 5a href="cic:/matita/basics/relations/monotonic.def(1)"
\ 6monotonic
\ 5/a
\ 6 ?
\ 5a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"
\ 6le
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"
\ 6pred
\ 5/a
\ 6.
238 #n #m #lenm (elim lenm) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
240 theorem le_S_S_to_le: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m → n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m.
242 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"
\ 6monotonic_pred
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
244 (* this are instances of the le versions
245 theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m.
248 theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
251 theorem lt_to_not_zero : ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m →
\ 5a href="cic:/matita/arithmetics/nat/not_zero.def(1)"
\ 6not_zero
\ 5/a
\ 6 m.
252 #n #m #Hlt (elim Hlt) // qed.
255 theorem not_le_Sn_O: ∀ n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"
\ 6≰
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6.
256 #n @
\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"
\ 6nmk
\ 5/a
\ 6 #Hlen0 @(
\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_zero.def(2)"
\ 6lt_to_not_zero
\ 5/a
\ 6 ?? Hlen0) qed.
258 theorem not_le_to_not_le_S_S: ∀ n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"
\ 6≰
\ 5/a
\ 6 m →
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"
\ 6≰
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m.
259 /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"
\ 6monotonic_pred
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
261 theorem not_le_S_S_to_not_le: ∀ n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"
\ 6≰
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m → n
\ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"
\ 6≰
\ 5/a
\ 6 m.
262 /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
264 theorem decidable_le: ∀n,m.
\ 5a href="cic:/matita/basics/logic/decidable.def(1)"
\ 6decidable
\ 5/a
\ 6 (n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6m).
265 @
\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"
\ 6nat_elim2
\ 5/a
\ 6 #n /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"
\ 6or_introl
\ 5/a
\ 6,
\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"
\ 6or_intror
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ #m * /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"
\ 6or_introl
\ 5/a
\ 6,
\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"
\ 6or_intror
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_not_le_S_S.def(5)"
\ 6not_le_to_not_le_S_S
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
267 theorem decidable_lt: ∀n,m.
\ 5a href="cic:/matita/basics/logic/decidable.def(1)"
\ 6decidable
\ 5/a
\ 6 (n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m).
268 #n #m @
\ 5a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"
\ 6decidable_le
\ 5/a
\ 6 qed.
270 theorem not_le_Sn_n: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"
\ 6≰
\ 5/a
\ 6 n.
271 #n (elim n) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_not_le_S_S.def(5)"
\ 6not_le_to_not_le_S_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
273 (* this is le_S_S_to_le
274 theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m.
278 lemma le_gen: ∀P:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 → Prop.∀n.(∀i. i
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n → P i) → P n.
279 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
281 theorem not_le_to_lt: ∀n,m. n
\ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"
\ 6≰
\ 5/a
\ 6 m → m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n.
282 @
\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"
\ 6nat_elim2
\ 5/a
\ 6 #n
283 [#abs @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
284 |/
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
285 |#m #Hind #HnotleSS @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/not_le_S_S_to_not_le.def(4)"
\ 6not_le_S_S_to_not_le
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
289 theorem lt_to_not_le: ∀n,m. n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m → m
\ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"
\ 6≰
\ 5/a
\ 6 n.
290 #n #m #Hltnm (elim Hltnm) /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
292 theorem not_lt_to_le: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'not less than'" href="cic:/fakeuri.def(1)"
\ 6≮
\ 5/a
\ 6 m → m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n.
293 /
\ 5span class="autotactic"
\ 64
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"
\ 6not_le_to_lt
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"
\ 6monotonic_pred
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
295 theorem le_to_not_lt: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → m
\ 5a title="natural 'not less than'" href="cic:/fakeuri.def(1)"
\ 6≮
\ 5/a
\ 6 n.
296 #n #m #H @
\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"
\ 6lt_to_not_le
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ (* /3/ *) qed.
298 (* lt and le trans *)
300 theorem lt_to_le_to_lt: ∀n,m,p:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m → m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 p → n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 p.
301 #n #m #p #H #H1 (elim H1) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"
\ 6transitive_lt
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
303 theorem le_to_lt_to_lt: ∀n,m,p:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 p → n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 p.
304 #n #m #p #H (elim H) /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"
\ 6transitive_lt
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
306 theorem lt_S_to_lt: ∀n,m.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m → n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m.
307 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"
\ 6transitive_lt
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
309 theorem ltn_to_ltO: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m →
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m.
310 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"
\ 6le_to_lt_to_lt
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
312 theorem lt_O_n_elim: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n →
313 ∀P:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 → Prop.(∀m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.P (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m)) → P n.
314 #n (elim n) // #abs @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
317 theorem S_pred: ∀n.
\ 5a title="natural number" href="cic:/fakeuri.def(1)"
\ 60
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n →
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6(
\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"
\ 6pred
\ 5/a
\ 6 n)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 n.
318 #n #posn (cases posn) //
322 theorem le_to_or_lt_eq: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m
\ 5a title="logical or" href="cic:/fakeuri.def(1)"
\ 6∨
\ 5/a
\ 6 n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m.
323 #n #m #lenm (elim lenm) /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"
\ 6or_introl
\ 5/a
\ 6,
\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"
\ 6or_intror
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"
\ 6le_to_lt_to_lt
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
326 theorem lt_to_not_eq : ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m → n
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 m.
327 #n #m #H @
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6,
\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"
\ 6nmk
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
329 theorem not_eq_to_le_to_lt: ∀n,m. n
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6m → n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6m → n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6m.
330 #n #m #Hneq #Hle cases (
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 ?? Hle) //
331 #Heq /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"
\ 6not_le_to_lt
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
333 nelim (Hneq Heq) qed. *)
336 theorem le_n_O_to_eq : ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6n.
337 #n (cases n) // #a #abs @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
339 theorem le_n_O_elim: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 → ∀P:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →Prop. P
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 → P n.
340 #n (cases n) // #a #abs @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
342 theorem le_n_Sm_elim : ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m →
343 ∀P:Prop. (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m → P) → (n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m → P) → P.
344 #n #m #Hle #P (elim Hle) /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
348 theorem le_to_le_to_eq: ∀n,m. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n → n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m.
349 @
\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"
\ 6nat_elim2
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 64
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"
\ 6eq_f
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le_n_O_to_eq.def(4)"
\ 6le_n_O_to_eq
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"
\ 6monotonic_pred
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
352 theorem lt_O_S : ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n.
353 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"
\ 6not_le_to_lt
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
356 (* other abstract properties *)
357 theorem antisymmetric_le : antisymmetric nat le.
358 unfold antisymmetric.intros 2.
359 apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
360 intros.apply le_n_O_to_eq.assumption.
361 intros.apply False_ind.apply (not_le_Sn_O ? H).
362 intros.apply eq_f.apply H.
363 apply le_S_S_to_le.assumption.
364 apply le_S_S_to_le.assumption.
367 theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
368 \def antisymmetric_le.
370 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
373 generalize in match (le_S_S_to_le ? ? H1)
380 (* well founded induction principles *)
382 theorem nat_elim1 : ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.∀P:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 → Prop.
383 (∀m.(∀p. p
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m → P p) → P m) → P n.
385 cut (∀q:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. q
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n → P q) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
387 [#q #HleO (* applica male *)
388 @(
\ 5a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"
\ 6le_n_O_elim
\ 5/a
\ 6 ? HleO)
389 @H #p #ltpO @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ (* 3 *)
391 @H #a #lta @Hind @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
395 (* some properties of functions *)
397 definition increasing ≝ λf:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. f n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 f (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n).
399 theorem increasing_to_monotonic: ∀f:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
400 \ 5a href="cic:/matita/arithmetics/nat/increasing.def(2)"
\ 6increasing
\ 5/a
\ 6 f →
\ 5a href="cic:/matita/basics/relations/monotonic.def(1)"
\ 6monotonic
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"
\ 6lt
\ 5/a
\ 6 f.
401 #f #incr #n #m #ltnm (elim ltnm) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"
\ 6transitive_lt
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
404 theorem le_n_fn: ∀f:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
405 \ 5a href="cic:/matita/arithmetics/nat/increasing.def(2)"
\ 6increasing
\ 5/a
\ 6 f → ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 f n.
406 #f #incr #n (elim n) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"
\ 6le_to_lt_to_lt
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
409 theorem increasing_to_le: ∀f:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
410 \ 5a href="cic:/matita/arithmetics/nat/increasing.def(2)"
\ 6increasing
\ 5/a
\ 6 f → ∀m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6∃
\ 5/a
\ 6i.m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 f i.
411 #f #incr #m (elim m) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"
\ 6ex_intro
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/#n * #a #lenfa
412 @(
\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"
\ 6ex_intro
\ 5/a
\ 6 ?? (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 a)) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"
\ 6le_to_lt_to_lt
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
415 theorem increasing_to_le2: ∀f:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/increasing.def(2)"
\ 6increasing
\ 5/a
\ 6 f →
416 ∀m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. f
\ 5a title="natural number" href="cic:/fakeuri.def(1)"
\ 60
\ 5/a
\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m →
\ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6∃
\ 5/a
\ 6i. f i
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 f (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 i).
417 #f #incr #m #lem (elim lem)
418 [@(
\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"
\ 6ex_intro
\ 5/a
\ 6 ? ?
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"
\ 6conj
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
419 |#n #len * #a * #len #ltnr (cases(
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … ltnr)) #H
420 [@(
\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"
\ 6ex_intro
\ 5/a
\ 6 ? ? a) % /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"
\ 6le_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
421 |@(
\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"
\ 6ex_intro
\ 5/a
\ 6 ? ? (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 a)) % //
426 theorem increasing_to_injective: ∀f:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
427 \ 5a href="cic:/matita/arithmetics/nat/increasing.def(2)"
\ 6increasing
\ 5/a
\ 6 f →
\ 5a href="cic:/matita/basics/relations/injective.def(1)"
\ 6injective
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 f.
428 #f #incr #n #m cases(
\ 5a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"
\ 6decidable_le
\ 5/a
\ 6 n m)
429 [#lenm cases(
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … lenm) //
430 #lenm #eqf @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … eqf) @
\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"
\ 6lt_to_not_eq
\ 5/a
\ 6
431 @
\ 5a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"
\ 6increasing_to_monotonic
\ 5/a
\ 6 //
432 |#nlenm #eqf @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … eqf) @
\ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"
\ 6sym_not_eq
\ 5/a
\ 6
433 @
\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"
\ 6lt_to_not_eq
\ 5/a
\ 6 @
\ 5a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"
\ 6increasing_to_monotonic
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"
\ 6not_le_to_lt
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
437 (*********************** monotonicity ***************************)
438 theorem monotonic_le_plus_r:
439 ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/basics/relations/monotonic.def(1)"
\ 6monotonic
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"
\ 6le
\ 5/a
\ 6 (λm.n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 m).
440 #n #a #b (elim n) normalize //
441 #m #H #leab @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/ qed.
444 theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m
445 ≝ monotonic_le_plus_r. *)
447 theorem monotonic_le_plus_l:
448 ∀m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/basics/relations/monotonic.def(1)"
\ 6monotonic
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"
\ 6le
\ 5/a
\ 6 (λn.n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 m).
449 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"
\ 6monotonic_le_plus_r
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
452 theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
453 \def monotonic_le_plus_l. *)
455 theorem le_plus: ∀n1,n2,m1,m2:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n1
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n2 → m1
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m2
456 → n1
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 m1
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n2
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 m2.
457 #n1 #n2 #m1 #m2 #len #lem @(
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6 ? (n1
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6m2))
458 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"
\ 6monotonic_le_plus_l
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"
\ 6monotonic_le_plus_r
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
460 theorem le_plus_n :∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 m.
461 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"
\ 6monotonic_le_plus_l
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
463 lemma le_plus_a: ∀a,n,m. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 a
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 m.
464 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus.def(7)"
\ 6le_plus
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
466 lemma le_plus_b: ∀b,n,m. n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m.
467 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
469 theorem le_plus_n_r :∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 n.
470 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/ qed.
472 theorem eq_plus_to_le: ∀n,m,p:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6m
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6p → m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n.
475 theorem le_plus_to_le: ∀a,n,m. a
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 a
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 m → n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m.
476 #a (elim a) normalize /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"
\ 6monotonic_pred
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
478 theorem le_plus_to_le_r: ∀a,n,m. n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 a
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6a → n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m.
479 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_le.def(5)"
\ 6le_plus_to_le
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
483 theorem monotonic_lt_plus_r:
484 ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/basics/relations/monotonic.def(1)"
\ 6monotonic
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"
\ 6lt
\ 5/a
\ 6 (λm.n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6m).
485 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"
\ 6increasing_to_monotonic
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
488 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
489 monotonic_lt_plus_r. *)
491 theorem monotonic_lt_plus_l:
492 ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/basics/relations/monotonic.def(1)"
\ 6monotonic
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"
\ 6lt
\ 5/a
\ 6 (λm.m
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6n).
493 (* /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"
\ 6increasing_to_monotonic
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ *) #n @
\ 5a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"
\ 6increasing_to_monotonic
\ 5/a
\ 6 // qed.
496 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
497 monotonic_lt_plus_l. *)
499 theorem lt_plus: ∀n,m,p,q:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m → p
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 q → n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 p
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 q.
500 #n #m #p #q #ltnm #ltpq
501 @(
\ 5a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"
\ 6transitive_lt
\ 5/a
\ 6 ? (n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6q))/
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"
\ 6monotonic_le_plus_r
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"
\ 6monotonic_lt_plus_l
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
503 theorem lt_plus_to_lt_l :∀n,p,q:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. p
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 q
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6n → p
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6q.
504 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_le.def(5)"
\ 6le_plus_to_le
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
506 theorem lt_plus_to_lt_r :∀n,p,q:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6p
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6q → p
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6q.
507 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_lt_l.def(6)"
\ 6lt_plus_to_lt_l
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
510 theorem le_to_lt_to_lt_plus: ∀a,b,c,d:nat.
511 a ≤ c → b < d → a + b < c+d.
512 (* bello /2/ un po' lento *)
513 #a #b #c #d #leac #lebd
514 normalize napplyS le_plus // qed.
518 theorem monotonic_le_times_r:
519 ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/basics/relations/monotonic.def(1)"
\ 6monotonic
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"
\ 6le
\ 5/a
\ 6 (λm. n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6 m).
520 #n #x #y #lexy (elim n) normalize//(* lento /2/*)
521 #a #lea @
\ 5a href="cic:/matita/arithmetics/nat/le_plus.def(7)"
\ 6le_plus
\ 5/a
\ 6 //
525 theorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m
526 \def monotonic_le_times_r. *)
529 theorem monotonic_le_times_l:
530 ∀m:nat.monotonic nat le (λn.n*m).
535 theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
536 \def monotonic_le_times_l. *)
538 theorem le_times: ∀n1,n2,m1,m2:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
539 n1
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n2 → m1
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m2 → n1
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6m1
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n2
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6m2.
540 #n1 #n2 #m1 #m2 #len #lem @(
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6 ? (n1
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6m2)) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"
\ 6monotonic_le_times_r
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
544 theorem lt_times_n: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6m.
545 #n #m #H /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"
\ 6monotonic_le_times_r
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
547 theorem le_times_to_le:
548 ∀a,n,m.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 a → a
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6 n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 a
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6 m → n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m.
549 #a @
\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"
\ 6nat_elim2
\ 5/a
\ 6 normalize
552 @(
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6 ? (a
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n)) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"
\ 6monotonic_le_times_r
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
554 @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6 @H /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_le.def(5)"
\ 6le_plus_to_le
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
559 theorem le_S_times_2: ∀n,m.O < m → n ≤ m → S n ≤ 2*m.
560 #n #m #posm #lenm (* interessante *)
561 applyS (le_plus n m) // qed. *)
565 theorem lt_O_times_S_S: ∀n,m:nat.O < (S n)*(S m).
566 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
570 theorem lt_times_eq_O: \forall a,b:nat.
571 O < a → a * b = O → b = O.
578 rewrite > (S_pred a) in H1
580 apply (eq_to_not_lt O ((S (pred a))*(S m)))
583 | apply lt_O_times_S_S
590 theorem O_lt_times_to_O_lt: \forall a,c:nat.
591 O \lt (a * c) \to O \lt a.
603 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
605 elim (le_to_or_lt_eq O ? (le_O_n m))
609 rewrite < times_n_O in H.
610 apply (not_le_Sn_O ? H)
615 theorem monotonic_lt_times_r:
616 ∀n:nat.monotonic nat lt (λm.(S n)*m).
620 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
621 apply lt_plus.assumption.assumption.
624 theorem monotonic_lt_times_r:
625 ∀c:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 c →
\ 5a href="cic:/matita/basics/relations/monotonic.def(1)"
\ 6monotonic
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"
\ 6lt
\ 5/a
\ 6 (λt.(c
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6t)).
627 (elim ltnm) normalize
628 [/
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"
\ 6monotonic_lt_plus_l
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
629 |#a #_ #lt1 @(
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6 … lt1) //
633 theorem monotonic_lt_times_l:
634 ∀c:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 c →
\ 5a href="cic:/matita/basics/relations/monotonic.def(1)"
\ 6monotonic
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"
\ 6lt
\ 5/a
\ 6 (λt.(t
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6c)).
635 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(10)"
\ 6monotonic_lt_times_r
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
638 theorem lt_to_le_to_lt_times:
639 ∀n,m,p,q:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m → p
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 q →
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 q → n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6p
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6q.
640 #n #m #p #q #ltnm #lepq #posq
641 @(
\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"
\ 6le_to_lt_to_lt
\ 5/a
\ 6 ? (n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6q))
642 [@
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"
\ 6monotonic_le_times_r
\ 5/a
\ 6 //
643 |@
\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(11)"
\ 6monotonic_lt_times_l
\ 5/a
\ 6 //
647 theorem lt_times:∀n,m,p,q:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6m → p
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6q → n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6p
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6q.
648 #n #m #p #q #ltnm #ltpq @
\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(12)"
\ 6lt_to_le_to_lt_times
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"
\ 6le_plus_b
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"
\ 6ltn_to_ltO
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
651 theorem lt_times_n_to_lt_l:
652 ∀n,p,q:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. p
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 q
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6n → p
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 q.
653 #n #p #q #Hlt (elim (
\ 5a href="cic:/matita/arithmetics/nat/decidable_lt.def(7)"
\ 6decidable_lt
\ 5/a
\ 6 p q)) //
654 #nltpq @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 ? ? (
\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"
\ 6lt_to_not_le
\ 5/a
\ 6 ? ? Hlt))
655 applyS
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"
\ 6monotonic_le_times_r
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/not_lt_to_le.def(6)"
\ 6not_lt_to_le
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
658 theorem lt_times_n_to_lt_r:
659 ∀n,p,q:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6p
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6q → p
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 q.
660 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/lt_times_n_to_lt_l.def(9)"
\ 6lt_times_n_to_lt_l
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
663 theorem nat_compare_times_l : \forall n,p,q:nat.
664 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
665 intros.apply nat_compare_elim.intro.
666 apply nat_compare_elim.
669 apply (inj_times_r n).assumption.
670 apply lt_to_not_eq. assumption.
672 apply (lt_times_to_lt_r n).assumption.
673 apply le_to_not_lt.apply lt_to_le.assumption.
674 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
675 intro.apply nat_compare_elim.intro.
677 apply (lt_times_to_lt_r n).assumption.
678 apply le_to_not_lt.apply lt_to_le.assumption.
681 apply (inj_times_r n).assumption.
682 apply lt_to_not_eq.assumption.
687 theorem lt_times_plus_times: \forall a,b,n,m:nat.
688 a < n \to b < m \to a*m + b < n*m.
691 [intros.apply False_ind.apply (not_le_Sn_O ? H)
695 change with (S b+a*m1 \leq m1+m*m1).
699 [apply le_S_S_to_le.assumption
706 (************************** minus ******************************)
710 [ O ⇒
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6
713 [ O ⇒
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 p
714 | S q ⇒ minus p q ]].
716 interpretation "natural minus" 'minus x y = (minus x y).
718 theorem minus_S_S: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m.
721 theorem minus_O_n: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6n.
724 theorem minus_n_O: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6.
727 theorem minus_n_n: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6n.
730 theorem minus_Sn_n: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n)
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6n.
731 #n (elim n) normalize // qed.
733 theorem minus_Sn_m: ∀m,n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n →
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m).
734 (* qualcosa da capire qui
735 #n #m #lenm nelim lenm napplyS refl_eq. *)
736 @
\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"
\ 6nat_elim2
\ 5/a
\ 6
738 |#n #abs @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
739 |#n #m #Hind #c applyS Hind /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"
\ 6monotonic_pred
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
744 theorem not_eq_to_le_to_le_minus:
745 ∀n,m.n ≠ m → n ≤ m → n ≤ m - 1.
746 #n * #m (cases m// #m normalize
747 #H #H1 napply le_S_S_to_le
748 napplyS (not_eq_to_le_to_lt n (S m) H H1)
751 theorem eq_minus_S_pred: ∀n,m. n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6 (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"
\ 6pred
\ 5/a
\ 6(n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m).
752 @
\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"
\ 6nat_elim2
\ 5/a
\ 6 normalize //
756 ∀m,n,p:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n → (n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m)
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6p
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 (n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6p)
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m.
757 @
\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"
\ 6nat_elim2
\ 5/a
\ 6
759 |#n #p #abs @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
760 |normalize/
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"
\ 6monotonic_pred
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
764 theorem minus_plus_m_m: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 (n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6m)
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m.
765 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"
\ 6plus_minus
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
767 theorem plus_minus_m_m: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
768 m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n → n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 (n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m)
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6m.
769 #n #m #lemn @
\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"
\ 6sym_eq
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"
\ 6plus_minus
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
771 theorem le_plus_minus_m_m: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 (n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m)
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6m.
772 #n (elim n) // #a #Hind #m (cases m) // normalize #n/
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
775 theorem minus_to_plus :∀n,m,p:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
776 m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n → n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 p → n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6p.
777 #n #m #p #lemn #eqp (applyS
\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"
\ 6plus_minus_m_m
\ 5/a
\ 6) //
780 theorem plus_to_minus :∀n,m,p:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6p → n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 p.
781 #n #m #p #eqp @
\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"
\ 6sym_eq
\ 5/a
\ 6 (applyS (
\ 5a href="cic:/matita/arithmetics/nat/minus_plus_m_m.def(6)"
\ 6minus_plus_m_m
\ 5/a
\ 6 p m))
784 theorem minus_pred_pred : ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n →
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m →
785 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"
\ 6pred
\ 5/a
\ 6 n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"
\ 6pred
\ 5/a
\ 6 m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6 m.
786 #n #m #posn #posm @(
\ 5a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"
\ 6lt_O_n_elim
\ 5/a
\ 6 n posn) @(
\ 5a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"
\ 6lt_O_n_elim
\ 5/a
\ 6 m posm) //.
792 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
793 intros.elim H.elim (minus_Sn_n n).apply le_n.
794 rewrite > minus_Sn_m.
795 apply le_S.assumption.
796 apply lt_to_le.assumption.
799 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
801 apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
802 intro.elim n1.simplify.apply le_n_Sn.
803 simplify.rewrite < minus_n_O.apply le_n.
804 intros.simplify.apply le_n_Sn.
805 intros.simplify.apply H.
808 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
811 (* end auto($Revision: 9739 $) proof: TIME=1.33 SIZE=100 DEPTH=100 *)
812 apply (trans_le (m-n) (S (m-(S n))) p).
813 apply minus_le_S_minus_S.
817 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
818 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)).
819 intros.rewrite < minus_n_O.apply le_n.
820 intros.simplify.apply le_n.
821 intros.simplify.apply le_S.assumption.
824 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
825 intros.apply (lt_O_n_elim n H).intro.
826 apply (lt_O_n_elim m H1).intro.
827 simplify.unfold lt.apply le_S_S.apply le_minus_m.
830 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
832 apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)).
834 simplify.intros. assumption.
835 simplify.intros.apply le_S_S.apply H.assumption.
839 (* monotonicity and galois *)
841 theorem monotonic_le_minus_l:
842 ∀p,q,n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. q
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 p → q
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 p
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6n.
843 @
\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"
\ 6nat_elim2
\ 5/a
\ 6 #p #q
844 [#lePO @(
\ 5a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"
\ 6le_n_O_elim
\ 5/a
\ 6 ? lePO) //
846 |#Hind #n (cases n) // #a #leSS @Hind /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"
\ 6monotonic_pred
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
850 theorem le_minus_to_plus: ∀n,m,p. n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 p → n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 p
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6m.
851 #n #m #p #lep @
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6
852 [|@
\ 5a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(9)"
\ 6le_plus_minus_m_m
\ 5/a
\ 6 | @
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"
\ 6monotonic_le_plus_l
\ 5/a
\ 6 // ]
855 theorem le_minus_to_plus_r: ∀a,b,c. c
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 b → a
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 b
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6 c → a
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 c
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 b.
856 #a #b #c #Hlecb #H >(
\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"
\ 6plus_minus_m_m
\ 5/a
\ 6 … Hlecb) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_minus_to_plus.def(10)"
\ 6le_minus_to_plus
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
859 theorem le_plus_to_minus: ∀n,m,p. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 p
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6m → n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 p.
860 #n #m #p #lep /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(9)"
\ 6monotonic_le_minus_l
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
862 theorem le_plus_to_minus_r: ∀a,b,c. a
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 c → a
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 c
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6b.
863 #a #b #c #H @(
\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_le_r.def(6)"
\ 6le_plus_to_le_r
\ 5/a
\ 6 … b) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
866 theorem lt_minus_to_plus: ∀a,b,c. a
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6 b
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 c → a
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 c
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b.
867 #a #b #c #H @
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"
\ 6not_le_to_lt
\ 5/a
\ 6
868 @(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"
\ 6lt_to_not_le
\ 5/a
\ 6 …H)) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"
\ 6le_plus_to_minus_r
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
871 theorem lt_minus_to_plus_r: ∀a,b,c. a
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 b
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6 c → a
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 c
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 b.
872 #a #b #c #H @
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"
\ 6not_le_to_lt
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"
\ 6le_plus_to_minus
\ 5/a
\ 6 …))
873 @
\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"
\ 6lt_to_not_le
\ 5/a
\ 6 //
876 theorem lt_plus_to_minus: ∀n,m,p. m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n → n
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 p
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6m → n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 p.
877 #n #m #p #lenm #H normalize <
\ 5a href="cic:/matita/arithmetics/nat/minus_Sn_m.def(5)"
\ 6minus_Sn_m
\ 5/a
\ 6 // @
\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"
\ 6le_plus_to_minus
\ 5/a
\ 6 //
880 theorem lt_plus_to_minus_r: ∀a,b,c. a
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 c → a
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 c
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6 b.
881 #a #b #c #H @
\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"
\ 6le_plus_to_minus_r
\ 5/a
\ 6 //
884 theorem monotonic_le_minus_r:
885 ∀p,q,n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. q
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 p → n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6p
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6q.
886 #p #q #n #lepq @
\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"
\ 6le_plus_to_minus
\ 5/a
\ 6
887 @(
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(9)"
\ 6le_plus_minus_m_m
\ 5/a
\ 6 ? q)) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"
\ 6monotonic_le_plus_r
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
890 theorem monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
892 @lt_plus_to_minus_r <plus_minus_m_m //
895 theorem eq_minus_O: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
896 n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6.
897 #n #m #lenm @(
\ 5a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"
\ 6le_n_O_elim
\ 5/a
\ 6 (n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m)) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_minus_r.def(11)"
\ 6monotonic_le_minus_r
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
900 theorem distributive_times_minus:
\ 5a href="cic:/matita/basics/relations/distributive.def(1)"
\ 6distributive
\ 5/a
\ 6 ?
\ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"
\ 6times
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/minus.fix(0,0,1)"
\ 6minus
\ 5/a
\ 6.
902 (cases (
\ 5a href="cic:/matita/arithmetics/nat/decidable_lt.def(7)"
\ 6decidable_lt
\ 5/a
\ 6 b c)) #Hbc
903 [>
\ 5a href="cic:/matita/arithmetics/nat/eq_minus_O.def(12)"
\ 6eq_minus_O
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"
\ 6le_plus_b
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ >
\ 5a href="cic:/matita/arithmetics/nat/eq_minus_O.def(12)"
\ 6eq_minus_O
\ 5/a
\ 6 //
904 @
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"
\ 6monotonic_le_times_r
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"
\ 6le_plus_b
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
905 |@
\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"
\ 6sym_eq
\ 5/a
\ 6 (applyS
\ 5a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"
\ 6plus_to_minus
\ 5/a
\ 6) <
\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus.def(7)"
\ 6distributive_times_plus
\ 5/a
\ 6
906 @
\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"
\ 6eq_f
\ 5/a
\ 6 (applyS
\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"
\ 6plus_minus_m_m
\ 5/a
\ 6) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/not_lt_to_le.def(6)"
\ 6not_lt_to_le
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
909 theorem minus_plus: ∀n,m,p. n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6p
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6(m
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6p).
911 cases (
\ 5a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"
\ 6decidable_le
\ 5/a
\ 6 (m
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6p) n) #Hlt
912 [@
\ 5a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"
\ 6plus_to_minus
\ 5/a
\ 6 @
\ 5a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"
\ 6plus_to_minus
\ 5/a
\ 6 <
\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"
\ 6associative_plus
\ 5/a
\ 6
913 @
\ 5a href="cic:/matita/arithmetics/nat/minus_to_plus.def(8)"
\ 6minus_to_plus
\ 5/a
\ 6 //
914 |cut (n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6p) [@(
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/arithmetics/nat/le_n_Sn.def(1)"
\ 6le_n_Sn
\ 5/a
\ 6 …)) @
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"
\ 6not_le_to_lt
\ 5/a
\ 6 //]
915 #H >
\ 5a href="cic:/matita/arithmetics/nat/eq_minus_O.def(12)"
\ 6eq_minus_O
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/eq_minus_O.def(12)"
\ 6eq_minus_O
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(9)"
\ 6monotonic_le_minus_l
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
920 theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
921 #n #m #p #lepm @plus_to_minus >(commutative_plus p)
922 >associative_plus <plus_minus_m_m //
925 theorem minus_minus: ∀n,m,p:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. p
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n →
926 p
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6(n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6m)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 n
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6(m
\ 5a title="natural minus" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6p).
928 @
\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"
\ 6sym_eq
\ 5/a
\ 6 @
\ 5a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"
\ 6plus_to_minus
\ 5/a
\ 6 <
\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"
\ 6associative_plus
\ 5/a
\ 6 <
\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"
\ 6plus_minus_m_m
\ 5/a
\ 6 //
929 <
\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"
\ 6commutative_plus
\ 5/a
\ 6 <
\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"
\ 6plus_minus_m_m
\ 5/a
\ 6 //
932 (*********************** boolean arithmetics ********************)
933 include "basics/bool.ma".
937 [ O ⇒ match m with [ O ⇒
\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 | S q ⇒
\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6]
938 | S p ⇒ match m with [ O ⇒
\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 | S q ⇒ eqb p q]
941 theorem eqb_elim : ∀ n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.∀ P:
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6 → Prop.
942 (n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6m → (P
\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6)) → (n
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 m → (P
\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6)) → (P (
\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"
\ 6eqb
\ 5/a
\ 6 n m)).
943 @
\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"
\ 6nat_elim2
\ 5/a
\ 6
944 [#n (cases n) normalize /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
945 |normalize /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"
\ 6sym_not_eq
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
946 |normalize /
\ 5span class="autotactic"
\ 64
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"
\ 6not_eq_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
950 theorem eqb_n_n: ∀n.
\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"
\ 6eqb
\ 5/a
\ 6 n n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6.
951 #n (elim n) normalize // qed.
953 theorem eqb_true_to_eq: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"
\ 6eqb
\ 5/a
\ 6 n m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 → n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m.
954 #n #m @(
\ 5a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"
\ 6eqb_elim
\ 5/a
\ 6 n m) // #_ #abs @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
956 theorem eqb_false_to_not_eq: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"
\ 6eqb
\ 5/a
\ 6 n m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 → n
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 m.
957 #n #m @(
\ 5a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"
\ 6eqb_elim
\ 5/a
\ 6 n m) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
959 theorem eq_to_eqb_true: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m →
\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"
\ 6eqb
\ 5/a
\ 6 n m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6.
962 theorem not_eq_to_eqb_false: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
963 n
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 m →
\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"
\ 6eqb
\ 5/a
\ 6 n m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6.
964 #n #m #noteq @
\ 5a href="cic:/matita/arithmetics/nat/eqb_elim.def(5)"
\ 6eqb_elim
\ 5/a
\ 6// #Heq @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
968 [ O ⇒
\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6
971 [ O ⇒
\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6
974 theorem leb_elim: ∀n,m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. ∀P:
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6 → Prop.
975 (n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → P
\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6) → (n
\ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"
\ 6≰
\ 5/a
\ 6 m → P
\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6) → P (
\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"
\ 6leb
\ 5/a
\ 6 n m).
976 @
\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"
\ 6nat_elim2
\ 5/a
\ 6 normalize
977 [/
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
978 |/
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
979 |#n #m #Hind #P #Pt #Pf @Hind
980 [#lenm @Pt @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6 // |#nlenm @Pf /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_not_le_S_S.def(5)"
\ 6not_le_to_not_le_S_S
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ ]
984 theorem leb_true_to_le:∀n,m.
\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"
\ 6leb
\ 5/a
\ 6 n m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 → n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m.
985 #n #m @
\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"
\ 6leb_elim
\ 5/a
\ 6 // #_ #abs @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
987 theorem leb_false_to_not_le:∀n,m.
988 \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"
\ 6leb
\ 5/a
\ 6 n m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 → n
\ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"
\ 6≰
\ 5/a
\ 6 m.
989 #n #m @
\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"
\ 6leb_elim
\ 5/a
\ 6 // #_ #abs @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
991 theorem le_to_leb_true: ∀n,m. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m →
\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"
\ 6leb
\ 5/a
\ 6 n m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6.
992 #n #m @
\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"
\ 6leb_elim
\ 5/a
\ 6 // #H #H1 @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
994 theorem not_le_to_leb_false: ∀n,m. n
\ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"
\ 6≰
\ 5/a
\ 6 m →
\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"
\ 6leb
\ 5/a
\ 6 n m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6.
995 #n #m @
\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"
\ 6leb_elim
\ 5/a
\ 6 // #H #H1 @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
997 theorem lt_to_leb_false: ∀n,m. m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n →
\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"
\ 6leb
\ 5/a
\ 6 n m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6.
998 /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"
\ 6lt_to_not_le
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"
\ 6not_le_to_leb_false
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
1001 ndefinition ltb ≝λn,m. leb (S n) m.
1003 theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
1004 (n < m → P true) → (n ≮ m → P false) → P (ltb n m).
1006 napply leb_elim /3/ qed.
1008 theorem ltb_true_to_lt:∀n,m.ltb n m = true → n < m.
1009 #n #m #Hltb napply leb_true_to_le nassumption
1012 theorem ltb_false_to_not_lt:∀n,m.
1013 ltb n m = false → n ≮ m.
1014 #n #m #Hltb napply leb_false_to_not_le nassumption
1017 theorem lt_to_ltb_true: ∀n,m. n < m → ltb n m = true.
1018 #n #m #Hltb napply le_to_leb_true nassumption
1021 theorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false.
1022 #n #m #Hltb napply lt_to_leb_false /2/
1026 definition min:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 ≝
1027 λn.λm. if (
\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"
\ 6leb
\ 5/a
\ 6 n m) then n else m.
1029 definition max:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 ≝
1030 λn.λm. if (
\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"
\ 6leb
\ 5/a
\ 6 n m) then m else n.
1032 lemma commutative_min:
\ 5a href="cic:/matita/basics/relations/commutative.def(1)"
\ 6commutative
\ 5/a
\ 6 ?
\ 5a href="cic:/matita/arithmetics/nat/min.def(2)"
\ 6min
\ 5/a
\ 6.
1033 #n #m normalize @
\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"
\ 6leb_elim
\ 5/a
\ 6
1034 [@
\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"
\ 6leb_elim
\ 5/a
\ 6 normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_to_le_to_eq.def(5)"
\ 6le_to_le_to_eq
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
1035 |#notle >(
\ 5a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"
\ 6le_to_leb_true
\ 5/a
\ 6 …) // @(
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m)) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"
\ 6not_le_to_lt
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
1038 lemma le_minr: ∀i,n,m. i
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/min.def(2)"
\ 6min
\ 5/a
\ 6 n m → i
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m.
1039 #i #n #m normalize @
\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"
\ 6leb_elim
\ 5/a
\ 6 normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
1041 lemma le_minl: ∀i,n,m. i
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/min.def(2)"
\ 6min
\ 5/a
\ 6 n m → i
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n.
1042 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_minr.def(7)"
\ 6le_minr
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
1044 lemma to_min: ∀i,n,m. i
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n → i
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → i
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/min.def(2)"
\ 6min
\ 5/a
\ 6 n m.
1045 #i #n #m #lein #leim normalize (cases (
\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"
\ 6leb
\ 5/a
\ 6 n m))
1048 lemma commutative_max:
\ 5a href="cic:/matita/basics/relations/commutative.def(1)"
\ 6commutative
\ 5/a
\ 6 ?
\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"
\ 6max
\ 5/a
\ 6.
1049 #n #m normalize @
\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"
\ 6leb_elim
\ 5/a
\ 6
1050 [@
\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"
\ 6leb_elim
\ 5/a
\ 6 normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_to_le_to_eq.def(5)"
\ 6le_to_le_to_eq
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
1051 |#notle >(
\ 5a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"
\ 6le_to_leb_true
\ 5/a
\ 6 …) // @(
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m)) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"
\ 6not_le_to_lt
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
1054 lemma le_maxl: ∀i,n,m.
\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"
\ 6max
\ 5/a
\ 6 n m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i → n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i.
1055 #i #n #m normalize @
\ 5a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"
\ 6leb_elim
\ 5/a
\ 6 normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
1057 lemma le_maxr: ∀i,n,m.
\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"
\ 6max
\ 5/a
\ 6 n m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i → m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i.
1058 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"
\ 6le_maxl
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
1060 lemma to_max: ∀i,n,m. n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i → m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i →
\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"
\ 6max
\ 5/a
\ 6 n m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i.
1061 #i #n #m #leni #lemi normalize (cases (
\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"
\ 6leb
\ 5/a
\ 6 n m))