From: matitaweb Date: Fri, 11 Nov 2011 16:13:34 +0000 (+0000) Subject: commit by user utente1 X-Git-Tag: make_still_working~2121 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=39dbed815d5a62c639ce9bb276fd44809053afb3;p=helm.git commit by user utente1 --- diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma index ef8da2f19..66ed6ccfd 100644 --- a/weblib/arithmetics/nat.ma +++ b/weblib/arithmetics/nat.ma @@ -33,7 +33,7 @@ theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m. //. qed. *) theorem not_eq_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a/span/span/ qed. definition not_zero: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. match n with [ O ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a | (S p) ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a ]. @@ -42,12 +42,12 @@ theorem not_eq_O_S : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"n #n @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #eqOS (change with (a href="cic:/matita/arithmetics/nat/not_zero.def(1)"not_zero/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a)) >eqOS // qed. theorem not_eq_n_Sn: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n. -#n (elim n) /2/ qed. +#n (elim n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"not_eq_S/a/span/span/ qed. theorem nat_case: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.∀P:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop. (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a → P a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) → (∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → P (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m)) → P n. -#n #P (elim n) /2/ qed. +#n #P (elim n) /span class="autotactic"2span class="autotrace" trace {}/span/span/ qed. theorem nat_elim2 : ∀R:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop. @@ -55,10 +55,10 @@ theorem nat_elim2 : → (∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) → (∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R n m → R (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m)) → ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R n m. -#R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /2/ qed. +#R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /span class="autotactic"2span class="autotrace" trace {}/span/span/ qed. theorem decidable_eq_nat : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/am). -@a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a #n [ (cases n) /2/ | /3/ | #m #Hind (cases Hind) /3/] +@a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a #n [ (cases n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a/span/span/ | #m #Hind (cases Hind) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"not_eq_S/a/span/span/] qed. (*************************** plus ******************************) @@ -102,7 +102,7 @@ theorem assoc_plus1: ∀a,b,c. c a title="natural plus" href="cic:/fakeuri.def( // qed. theorem injective_plus_r: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (λm.na title="natural plus" href="cic:/fakeuri.def(1)"+/am). -#n (elim n) normalize /3/ qed. +#n (elim n) normalize /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a/span/span/ qed. (* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m \def injective_plus_r. @@ -208,7 +208,7 @@ interpretation "natural 'greater than'" 'gt x y = (gt x y). interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)). theorem transitive_le : a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a. -#a #b #c #leab #lebc (elim lebc) /2/ +#a #b #c #leab #lebc (elim lebc) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed. (* @@ -216,30 +216,30 @@ theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p \def transitive_le. *) theorem transitive_lt: a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a. -#a #b #c #ltab #ltbc (elim ltbc) /2/qed. +#a #b #c #ltab #ltbc (elim ltbc) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/qed. (* theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p \def transitive_lt. *) theorem le_S_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m. -#n #m #lenm (elim lenm) /2/ qed. +#n #m #lenm (elim lenm) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed. theorem le_O_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. -#n (elim n) /2/ qed. +#n (elim n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed. theorem le_n_Sn : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed. theorem le_pred_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. #n (elim n) // qed. theorem monotonic_pred: a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a ? a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a. -#n #m #lenm (elim lenm) /2/ qed. +#n #m #lenm (elim lenm) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed. theorem le_S_S_to_le: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. (* demo *) -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ qed. (* this are instances of the le versions theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m. @@ -256,19 +256,19 @@ theorem not_le_Sn_O: ∀ n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)" #n @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Hlen0 @(a href="cic:/matita/arithmetics/nat/lt_to_not_zero.def(2)"lt_to_not_zero/a ?? Hlen0) qed. theorem not_le_to_not_le_S_S: ∀ n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m. -/3/ qed. +/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ qed. theorem not_le_S_S_to_not_le: ∀ n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m. -/3/ qed. +/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a/span/span/ qed. theorem decidable_le: ∀n,m. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am). -@a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a #n /2/ #m * /3/ qed. +@a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a #n /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ #m * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/arithmetics/nat/not_le_to_not_le_S_S.def(5)"not_le_to_not_le_S_S/a, a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a/span/span/ qed. theorem decidable_lt: ∀n,m. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m). #n #m @a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a qed. theorem not_le_Sn_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a n. -#n (elim n) /2/ qed. +#n (elim n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_le_to_not_le_S_S.def(5)"not_le_to_not_le_S_S/a/span/span/ qed. (* this is le_S_S_to_le theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m. @@ -276,38 +276,38 @@ theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m. *) lemma le_gen: ∀P:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop.∀n.(∀i. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → P i) → P n. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed. theorem not_le_to_lt: ∀n,m. n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a m → m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n. @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a #n - [#abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ - |/2/ - |#m #Hind #HnotleSS @a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a /3/ + [#abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + |/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a/span/span/ + |#m #Hind #HnotleSS @a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_le_S_S_to_not_le.def(4)"not_le_S_S_to_not_le/a/span/span/ ] qed. theorem lt_to_not_le: ∀n,m. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → m a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a n. -#n #m #Hltnm (elim Hltnm) /3/ qed. +#n #m #Hltnm (elim Hltnm) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a/span/span/ qed. theorem not_lt_to_le: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'not less than'" href="cic:/fakeuri.def(1)"≮/a m → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. -/4/ qed. +/span class="autotactic"4span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a, a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ qed. theorem le_to_not_lt: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → m a title="natural 'not less than'" href="cic:/fakeuri.def(1)"≮/a n. -#n #m #H @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a /2/ (* /3/ *) qed. +#n #m #H @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a/span/span/ (* /3/ *) qed. (* lt and le trans *) theorem lt_to_le_to_lt: ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p. -#n #m #p #H #H1 (elim H1) /2/ qed. +#n #m #p #H #H1 (elim H1) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed. theorem le_to_lt_to_lt: ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p. -#n #m #p #H (elim H) /3/ qed. +#n #m #p #H (elim H) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed. theorem lt_S_to_lt: ∀n,m. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed. theorem ltn_to_ltO: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a/span/span/ qed. (* theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat. @@ -322,7 +322,7 @@ qed. *) theorem lt_O_n_elim: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → ∀P:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop.(∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.P (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m)) → P n. -#n (elim n) // #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ +#n (elim n) // #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed. theorem S_pred: ∀n. a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n. @@ -357,11 +357,11 @@ qed. (* le to lt or eq *) theorem le_to_or_lt_eq: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m a title="logical or" href="cic:/fakeuri.def(1)"∨/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m. -#n #m #lenm (elim lenm) /3/ qed. +#n #m #lenm (elim lenm) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed. (* not eq *) theorem lt_to_not_eq : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m. -#n #m #H @a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a /2/ qed. +#n #m #H @a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a, a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a/span/span/ qed. (*not lt theorem eq_to_not_lt: ∀a,b:nat. a = b → a ≮ b. @@ -389,30 +389,30 @@ apply (not_le_Sn_n ? H3). qed. *) theorem not_eq_to_le_to_lt: ∀n,m. na title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/am → na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am → na title="natural 'less than'" href="cic:/fakeuri.def(1)"</am. -#n #m #Hneq #Hle cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(6)"le_to_or_lt_eq/a ?? Hle) // -#Heq /3/ qed. +#n #m #Hneq #Hle cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a ?? Hle) // +#Heq /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a, a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a/span/span/ qed. (* nelim (Hneq Heq) qed. *) (* le elimination *) theorem le_n_O_to_eq : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/an. -#n (cases n) // #a #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ qed. +#n (cases n) // #a #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed. theorem le_n_O_elim: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a → ∀P: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a →Prop. P a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a → P n. -#n (cases n) // #a #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ qed. +#n (cases n) // #a #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed. theorem le_n_Sm_elim : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → ∀P:Prop. (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → P) → (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → P) → P. -#n #m #Hle #P (elim Hle) /3/ qed. +#n #m #Hle #P (elim Hle) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a/span/span/ qed. (* le and eq *) theorem le_to_le_to_eq: ∀n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m. -@a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a /4/ +@a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a /span class="autotactic"4span class="autotrace" trace a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a, a href="cic:/matita/arithmetics/nat/le_n_O_to_eq.def(4)"le_n_O_to_eq/a, a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ qed. theorem lt_O_S : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a/span/span/ qed. (* (* other abstract properties *) @@ -444,13 +444,13 @@ qed. theorem nat_elim1 : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.∀P:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop. (∀m.(∀p. p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → P p) → P m) → P n. #n #P #H -cut (∀q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. q a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → P q) /2/ +cut (∀q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. q a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → P q) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ (elim n) [#q #HleO (* applica male *) @(a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"le_n_O_elim/a ? HleO) - @H #p #ltpO @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ (* 3 *) + @H #p #ltpO @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ (* 3 *) |#p #Hind #q #HleS - @H #a #lta @Hind @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a /2/ + @H #a #lta @Hind @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a/span/span/ ] qed. @@ -460,26 +460,26 @@ definition increasing ≝ λf:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0 theorem increasing_to_monotonic: ∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/increasing.def(2)"increasing/a f → a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a f. -#f #incr #n #m #ltnm (elim ltnm) /2/ +#f #incr #n #m #ltnm (elim ltnm) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a/span/span/ qed. theorem le_n_fn: ∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/increasing.def(2)"increasing/a f → ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a f n. -#f #incr #n (elim n) /2/ +#f #incr #n (elim n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a/span/span/ qed. theorem increasing_to_le: ∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/increasing.def(2)"increasing/a f → ∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a title="exists" href="cic:/fakeuri.def(1)"∃/ai.m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a f i. -#f #incr #m (elim m) /2/#n * #a #lenfa -@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ?? (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a a)) /2/ +#f #incr #m (elim m) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a/span/span/#n * #a #lenfa +@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ?? (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a a)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a/span/span/ qed. theorem increasing_to_le2: ∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/increasing.def(2)"increasing/a f → ∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. f a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a title="exists" href="cic:/fakeuri.def(1)"∃/ai. f i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m a title="logical and" href="cic:/fakeuri.def(1)"∧/a m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i). #f #incr #m #lem (elim lem) - [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ? ? a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) /2/ - |#n #len * #a * #len #ltnr (cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(6)"le_to_or_lt_eq/a … ltnr)) #H - [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ? ? a) % /2/ + [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ? ? a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ + |#n #len * #a * #len #ltnr (cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … ltnr)) #H + [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ? ? a) % /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ |@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ? ? (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a a)) % // ] ] @@ -488,11 +488,11 @@ qed. theorem increasing_to_injective: ∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/increasing.def(2)"increasing/a f → a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a f. #f #incr #n #m cases(a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a n m) - [#lenm cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(6)"le_to_or_lt_eq/a … lenm) // + [#lenm cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … lenm) // #lenm #eqf @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … eqf) @a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"lt_to_not_eq/a @a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a // |#nlenm #eqf @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … eqf) @a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a - @a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"lt_to_not_eq/a @a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a /2/ + @a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"lt_to_not_eq/a @a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a/span/span/ ] qed. @@ -500,7 +500,7 @@ qed. theorem monotonic_le_plus_r: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a (λm.n a title="natural plus" href="cic:/fakeuri.def(1)"+/a m). #n #a #b (elim n) normalize // -#m #H #leab @a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a /2/ qed. +#m #H #leab @a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a /span class="autotactic"2span class="autotrace" trace {}/span/span/ qed. (* theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m @@ -508,7 +508,7 @@ theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m theorem monotonic_le_plus_l: ∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a (λn.n a title="natural plus" href="cic:/fakeuri.def(1)"+/a m). -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/ qed. (* theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p @@ -517,34 +517,34 @@ theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p theorem le_plus: ∀n1,n2,m1,m2:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n2 → m1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m2 → n1 a title="natural plus" href="cic:/fakeuri.def(1)"+/a m1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n2 a title="natural plus" href="cic:/fakeuri.def(1)"+/a m2. #n1 #n2 #m1 #m2 #len #lem @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (n1a title="natural plus" href="cic:/fakeuri.def(1)"+/am2)) -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a, a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/ qed. theorem le_plus_n :∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a m. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a/span/span/ qed. lemma le_plus_a: ∀a,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a a title="natural plus" href="cic:/fakeuri.def(1)"+/a m. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus.def(7)"le_plus/a/span/span/ qed. lemma le_plus_b: ∀b,n,m. n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a/span/span/ qed. theorem le_plus_n_r :∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m a title="natural plus" href="cic:/fakeuri.def(1)"+/a n. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace {}/span/span/ qed. theorem eq_plus_to_le: ∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ama title="natural plus" href="cic:/fakeuri.def(1)"+/ap → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. // qed. theorem le_plus_to_le: ∀a,n,m. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a a title="natural plus" href="cic:/fakeuri.def(1)"+/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. -#a (elim a) normalize /3/ qed. +#a (elim a) normalize /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ qed. theorem le_plus_to_le_r: ∀a,n,m. n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m a title="natural plus" href="cic:/fakeuri.def(1)"+/aa → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_le.def(5)"le_plus_to_le/a/span/span/ qed. (* plus & lt *) theorem monotonic_lt_plus_r: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a (λm.na title="natural plus" href="cic:/fakeuri.def(1)"+/am). -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a/span/span/ qed. (* variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def @@ -552,7 +552,7 @@ monotonic_lt_plus_r. *) theorem monotonic_lt_plus_l: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a (λm.ma title="natural plus" href="cic:/fakeuri.def(1)"+/an). -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a/span/span/ qed. (* variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def @@ -560,13 +560,13 @@ monotonic_lt_plus_l. *) theorem lt_plus: ∀n,m,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q → n a title="natural plus" href="cic:/fakeuri.def(1)"+/a p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m a title="natural plus" href="cic:/fakeuri.def(1)"+/a q. #n #m #p #q #ltnm #ltpq -@(a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a ? (na title="natural plus" href="cic:/fakeuri.def(1)"+/aq))/2/ qed. +@(a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a ? (na title="natural plus" href="cic:/fakeuri.def(1)"+/aq))/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"monotonic_lt_plus_l/a, a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/ qed. theorem lt_plus_to_lt_l :∀n,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. pa title="natural plus" href="cic:/fakeuri.def(1)"+/an a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a qa title="natural plus" href="cic:/fakeuri.def(1)"+/an → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_le.def(5)"le_plus_to_le/a/span/span/ qed. theorem lt_plus_to_lt_r :∀n,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural plus" href="cic:/fakeuri.def(1)"+/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a na title="natural plus" href="cic:/fakeuri.def(1)"+/aq → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_plus_to_lt_l.def(6)"lt_plus_to_lt_l/a/span/span/ qed. (* theorem le_to_lt_to_lt_plus: ∀a,b,c,d:nat. @@ -599,21 +599,21 @@ theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p theorem le_times: ∀n1,n2,m1,m2:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n2 → m1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m2 → n1a title="natural times" href="cic:/fakeuri.def(1)"*/am1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n2a title="natural times" href="cic:/fakeuri.def(1)"*/am2. -#n1 #n2 #m1 #m2 #len #lem @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (n1a title="natural times" href="cic:/fakeuri.def(1)"*/am2)) /2/ +#n1 #n2 #m1 #m2 #len #lem @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (n1a title="natural times" href="cic:/fakeuri.def(1)"*/am2)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a/span/span/ qed. (* interessante *) theorem lt_times_n: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a na title="natural times" href="cic:/fakeuri.def(1)"*/am. -#n #m #H /2/ qed. +#n #m #H /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a/span/span/ qed. theorem le_times_to_le: ∀a,n,m. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a → a a title="natural times" href="cic:/fakeuri.def(1)"*/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a a title="natural times" href="cic:/fakeuri.def(1)"*/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. #a @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a normalize [// |#n #H1 #H2 - @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (aa title="natural times" href="cic:/fakeuri.def(1)"*/aa href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)) /2/ + @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (aa title="natural times" href="cic:/fakeuri.def(1)"*/aa href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a/span/span/ |#n #m #H #lta #le - @a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a @H /2/ + @a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a @H /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_le.def(5)"le_plus_to_le/a/span/span/ ] qed. @@ -687,39 +687,39 @@ theorem monotonic_lt_times_r: ∀c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a (λt.(ca title="natural times" href="cic:/fakeuri.def(1)"*/at)). #c #posc #n #m #ltnm (elim ltnm) normalize - [/2/ + [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"monotonic_lt_plus_l/a/span/span/ |#a #_ #lt1 @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … lt1) // ] qed. theorem monotonic_lt_times_l: ∀c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a (λt.(ta title="natural times" href="cic:/fakeuri.def(1)"*/ac)). -/2/ +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(10)"monotonic_lt_times_r/a/span/span/ qed. theorem lt_to_le_to_lt_times: ∀n,m,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → p a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a q → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q → na title="natural times" href="cic:/fakeuri.def(1)"*/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a ma title="natural times" href="cic:/fakeuri.def(1)"*/aq. #n #m #p #q #ltnm #lepq #posq -@(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(5)"le_to_lt_to_lt/a ? (na title="natural times" href="cic:/fakeuri.def(1)"*/aq)) +@(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a ? (na title="natural times" href="cic:/fakeuri.def(1)"*/aq)) [@a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a // - |@a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(10)"monotonic_lt_times_l/a // + |@a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(11)"monotonic_lt_times_l/a // ] qed. theorem lt_times:∀n,m,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural 'less than'" href="cic:/fakeuri.def(1)"</am → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq → na title="natural times" href="cic:/fakeuri.def(1)"*/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a ma title="natural times" href="cic:/fakeuri.def(1)"*/aq. -#n #m #p #q #ltnm #ltpq @a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"lt_to_le_to_lt_times/aspan style="text-decoration: underline;" /span/2/ +#n #m #p #q #ltnm #ltpq @a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(12)"lt_to_le_to_lt_times/aspan style="text-decoration: underline;" /span/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a, a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"ltn_to_ltO/a/span/span/ qed. theorem lt_times_n_to_lt_l: ∀n,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. pa title="natural times" href="cic:/fakeuri.def(1)"*/an a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a qa title="natural times" href="cic:/fakeuri.def(1)"*/an → p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q. #n #p #q #Hlt (elim (a href="cic:/matita/arithmetics/nat/decidable_lt.def(7)"decidable_lt/a p q)) // #nltpq @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a ? ? (a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a ? ? Hlt)) -applyS a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a /2/ +applyS a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_lt_to_le.def(6)"not_lt_to_le/a/span/span/ qed. theorem lt_times_n_to_lt_r: ∀n,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural times" href="cic:/fakeuri.def(1)"*/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a na title="natural times" href="cic:/fakeuri.def(1)"*/aq → p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/lt_times_n_to_lt_l.def(9)"lt_times_n_to_lt_l/a/span/span/ qed. (* theorem nat_compare_times_l : \forall n,p,q:nat. @@ -797,8 +797,8 @@ theorem minus_Sn_m: ∀m,n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)" #n #m #lenm nelim lenm napplyS refl_eq. *) @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a [// - |#n #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ - |#n #m #Hind #c applyS Hind /2/ + |#n #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + |#n #m #Hind #c applyS Hind /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ ] qed. @@ -818,20 +818,20 @@ theorem plus_minus: ∀m,n,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)a title="natural plus" href="cic:/fakeuri.def(1)"+/ap a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/ap)a title="natural minus" href="cic:/fakeuri.def(1)"-/am. @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a [// - |#n #p #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ - |normalize/3/ + |#n #p #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + |normalize/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ ] qed. theorem minus_plus_m_m: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/am)a title="natural minus" href="cic:/fakeuri.def(1)"-/am. -/2/ qed. +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"plus_minus/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed. theorem plus_minus_m_m: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)a title="natural plus" href="cic:/fakeuri.def(1)"+/am. -#n #m #lemn @a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a /2/ qed. +#n #m #lemn @a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/plus_minus.def(5)"plus_minus/a/span/span/ qed. theorem le_plus_minus_m_m: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)a title="natural plus" href="cic:/fakeuri.def(1)"+/am. -#n (elim n) // #a #Hind #m (cases m) // normalize #n/2/ +#n (elim n) // #a #Hind #m (cases m) // normalize #n/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a/span/span/ qed. theorem minus_to_plus :∀n,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. @@ -845,7 +845,7 @@ qed. theorem minus_pred_pred : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/a m. -#n #m #posn #posm @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(7)"lt_O_n_elim/a n posn) @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(7)"lt_O_n_elim/a m posm) //. +#n #m #posn #posm @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"lt_O_n_elim/a n posn) @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"lt_O_n_elim/a m posm) //. qed. @@ -905,62 +905,62 @@ theorem monotonic_le_minus_l: @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a #p #q [#lePO @(a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"le_n_O_elim/a ? lePO) // |// - |#Hind #n (cases n) // #a #leSS @Hind /2/ + |#Hind #n (cases n) // #a #leSS @Hind /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ ] qed. theorem le_minus_to_plus: ∀n,m,p. na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am. #n #m #p #lep @a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a - [|@a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(8)"le_plus_minus_m_m/a | @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a // ] + [|@a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(9)"le_plus_minus_m_m/a | @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a // ] qed. theorem le_minus_to_plus_r: ∀a,b,c. c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b → a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b. -#a #b #c #Hlecb #H >(a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a … Hlecb) /2/ +#a #b #c #Hlecb #H >(a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a … Hlecb) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a/span/span/ qed. theorem le_plus_to_minus: ∀n,m,p. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p. -#n #m #p #lep /2/ qed. +#n #m #p #lep /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(10)"monotonic_le_minus_l/a/span/span/ qed. theorem le_plus_to_minus_r: ∀a,b,c. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a c → a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a c a title="natural minus" href="cic:/fakeuri.def(1)"-/ab. -#a #b #c #H @(a href="cic:/matita/arithmetics/nat/le_plus_to_le_r.def(6)"le_plus_to_le_r/a … b) /2/ +#a #b #c #H @(a href="cic:/matita/arithmetics/nat/le_plus_to_le_r.def(6)"le_plus_to_le_r/a … b) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a/span/span/ qed. theorem lt_minus_to_plus: ∀a,b,c. a a title="natural minus" href="cic:/fakeuri.def(1)"-/a b a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c a title="natural plus" href="cic:/fakeuri.def(1)"+/a b. #a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a -@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a …H)) /2/ +@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a …H)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"le_plus_to_minus_r/a/span/span/ qed. theorem lt_minus_to_plus_r: ∀a,b,c. a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b. -#a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(9)"le_plus_to_minus/a …)) +#a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(11)"le_plus_to_minus/a …)) @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a // qed. theorem lt_plus_to_minus: ∀n,m,p. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p. -#n #m #p #lenm #H normalize <a href="cic:/matita/arithmetics/nat/minus_Sn_m.def(5)"minus_Sn_m/a // @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(9)"le_plus_to_minus/a // +#n #m #p #lenm #H normalize <a href="cic:/matita/arithmetics/nat/minus_Sn_m.def(5)"minus_Sn_m/a // @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(11)"le_plus_to_minus/a // qed. theorem lt_plus_to_minus_r: ∀a,b,c. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c a title="natural minus" href="cic:/fakeuri.def(1)"-/a b. -#a #b #c #H @a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(9)"le_plus_to_minus_r/a // +#a #b #c #H @a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"le_plus_to_minus_r/a // qed. theorem monotonic_le_minus_r: ∀p,q,n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. q a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural minus" href="cic:/fakeuri.def(1)"-/ap a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a na title="natural minus" href="cic:/fakeuri.def(1)"-/aq. -#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(9)"le_plus_to_minus/a -@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(8)"le_plus_minus_m_m/a ? q)) /2/ +#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(11)"le_plus_to_minus/a +@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(9)"le_plus_minus_m_m/a ? q)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/ qed. theorem eq_minus_O: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. -#n #m #lenm @(a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"le_n_O_elim/a (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)) /2/ +#n #m #lenm @(a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"le_n_O_elim/a (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_minus_r.def(12)"monotonic_le_minus_r/a/span/span/ qed. theorem distributive_times_minus: a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a ? a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/minus.fix(0,0,1)"minus/a. #a #b #c (cases (a href="cic:/matita/arithmetics/nat/decidable_lt.def(7)"decidable_lt/a b c)) #Hbc - [> a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"eq_minus_O/a /2/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"eq_minus_O/a // - @a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a /2/ + [> a href="cic:/matita/arithmetics/nat/eq_minus_O.def(13)"eq_minus_O/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(13)"eq_minus_O/a // + @a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ |@a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a (applyS a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a) <a href="cic:/matita/arithmetics/nat/distributive_times_plus.def(7)"distributive_times_plus/a - @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a (applyS a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a) /2/ + @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a (applyS a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_lt_to_le.def(6)"not_lt_to_le/a/span/span/ qed. theorem minus_plus: ∀n,m,p. na title="natural minus" href="cic:/fakeuri.def(1)"-/ama title="natural minus" href="cic:/fakeuri.def(1)"-/ap a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/a(ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap). @@ -969,7 +969,7 @@ cases (a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a [@a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a @a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a <a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a @a href="cic:/matita/arithmetics/nat/minus_to_plus.def(8)"minus_to_plus/a // |cut (n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap) [@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_n_Sn.def(1)"le_n_Sn/a …)) @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a //] - #H >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"eq_minus_O/a /2/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"eq_minus_O/a // + #H >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(13)"eq_minus_O/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/eq_minus_O.def(13)"eq_minus_O/a, a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(10)"monotonic_le_minus_l/a/span/span/ ] qed. @@ -979,11 +979,11 @@ theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p). >associative_plus (a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"le_to_leb_true/a …) // @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m)) /2/ +lemma commutative_min: commutative ? min. +#n #m normalize @leb_elim + [@leb_elim normalize /2/ + |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/ ] qed. -lemma le_minr: ∀i,n,m. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/min.def(2)"min/a n m → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. -#i #n #m normalize @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a normalize /2/ qed. +lemma le_minr: ∀i,n,m. i ≤ min n m → i ≤ m. +#i #n #m normalize @leb_elim normalize /2/ qed. -lemma le_minl: ∀i,n,m. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/min.def(2)"min/a n m → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. +lemma le_minl: ∀i,n,m. i ≤ min n m → i ≤ n. /2/ qed. -lemma to_min: ∀i,n,m. i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/min.def(2)"min/a n m. -#i #n #m #lein #leim normalize (cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m)) +lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m. +#i #n #m #lein #leim normalize (cases (leb n m)) normalize // qed. -lemma commutative_max: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/max.def(2)"max/a. -#n #m normalize @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a - [@a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a normalize /2/ - |#notle >(a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"le_to_leb_true/a …) // @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m)) /2/ +lemma commutative_max: commutative ? max. +#n #m normalize @leb_elim + [@leb_elim normalize /2/ + |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/ ] qed. -lemma le_maxl: ∀i,n,m. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i. -#i #n #m normalize @a href="cic:/matita/arithmetics/nat/leb_elim.def(6)"leb_elim/a normalize /2/ qed. +lemma le_maxl: ∀i,n,m. max n m ≤ i → n ≤ i. +#i #n #m normalize @leb_elim normalize /2/ qed. -lemma le_maxr: ∀i,n,m. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i. +lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i. /2/ qed. -lemma to_max: ∀i,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i. -#i #n #m #leni #lemi normalize (cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m)) +lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i. +#i #n #m #leni #lemi normalize (cases (leb n m)) normalize // qed. \ No newline at end of file