From b743e4f63f52be49ceb01646c8f1574d89817118 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 12 Sep 2011 11:36:38 +0000 Subject: [PATCH] commit by user utente1 --- weblib/arithmetics/nat.ma | 573 +++++++++++++++++++------------------- 1 file changed, 286 insertions(+), 287 deletions(-) diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma index 6fa6d57a8..f14392e93 100644 --- a/weblib/arithmetics/nat.ma +++ b/weblib/arithmetics/nat.ma @@ -20,55 +20,55 @@ interpretation "Natural numbers" 'N = nat. alias num (instance 0) = "natural number". definition pred ≝ - λn. match n with [ O ⇒ O | S p ⇒ p]. + λn. match n with [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a | S p ⇒ p]. -theorem pred_Sn : ∀n.n = pred (S n). +theorem pred_Sn : ∀n.n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n). // qed. -theorem injective_S : injective nat nat S. +theorem injective_S : 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 a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a. // qed. (* theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m. //. qed. *) -theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m. +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. -definition not_zero: nat → Prop ≝ - λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ]. +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 ]. -theorem not_eq_O_S : ∀n:nat. O ≠ S n. -#n @nmk #eqOS (change with (not_zero O)) >eqOS // qed. +theorem not_eq_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="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 @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:nat. n ≠ S n. +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. theorem nat_case: - ∀n:nat.∀P:nat → Prop. - (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n. + ∀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. theorem nat_elim2 : - ∀R:nat → nat → Prop. - (∀n:nat. R O n) - → (∀n:nat. R (S n) O) - → (∀n,m:nat. R n m → R (S n) (S m)) - → ∀n,m:nat. R n m. + ∀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. + (∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a n) + → (∀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. -theorem decidable_eq_nat : ∀n,m:nat.decidable (n=m). -@nat_elim2 #n [ (cases n) /2/ | /3/ | #m #Hind (cases Hind) /3/] +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/] qed. (*************************** plus ******************************) let rec plus n m ≝ - match n with [ O ⇒ m | S p ⇒ S (plus p m) ]. + match n with [ O ⇒ m | S p ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (plus p m) ]. interpretation "natural plus" 'plus x y = (plus x y). -theorem plus_O_n: ∀n:nat. n = O+n. +theorem plus_O_n: ∀n: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 a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural plus" href="cic:/fakeuri.def(1)"+/an. // qed. (* @@ -76,10 +76,10 @@ theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m. // qed. *) -theorem plus_n_O: ∀n:nat. n = n+0. +theorem plus_n_O: ∀n: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)"+/aa title="natural number" href="cic:/fakeuri.def(1)"0/a. #n (elim n) normalize // qed. -theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m. +theorem plus_n_Sm : ∀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 (na title="natural plus" href="cic:/fakeuri.def(1)"+/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m. #n (elim n) normalize // qed. (* @@ -92,16 +92,16 @@ theorem plus_n_1 : ∀n:nat. S n = n+1. // qed. *) -theorem commutative_plus: commutative ? plus. +theorem commutative_plus: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a. #n (elim n) normalize // qed. -theorem associative_plus : associative nat plus. +theorem associative_plus : a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a. #n (elim n) normalize // qed. -theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a. +theorem assoc_plus1: ∀a,b,c. c a title="natural plus" href="cic:/fakeuri.def(1)"+/a (b a title="natural plus" href="cic:/fakeuri.def(1)"+/a a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural plus" href="cic:/fakeuri.def(1)"+/a a. // qed. -theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m). +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. (* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m @@ -116,42 +116,42 @@ theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m). (*************************** times *****************************) let rec times n m ≝ - match n with [ O ⇒ O | S p ⇒ m+(times p m) ]. + match n with [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a | S p ⇒ ma title="natural plus" href="cic:/fakeuri.def(1)"+/a(times p m) ]. interpretation "natural times" 'times x y = (times x y). -theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m. +theorem times_Sn_m: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. ma title="natural plus" href="cic:/fakeuri.def(1)"+/ana title="natural times" 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,2,0)"S/a na title="natural times" href="cic:/fakeuri.def(1)"*/am. // qed. -theorem times_O_n: ∀n:nat. O = O*n. +theorem times_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="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural times" href="cic:/fakeuri.def(1)"*/an. // qed. -theorem times_n_O: ∀n:nat. O = n*O. +theorem times_n_O: ∀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="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. #n (elim n) // qed. -theorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m). +theorem times_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural plus" href="cic:/fakeuri.def(1)"+/a(na title="natural times" href="cic:/fakeuri.def(1)"*/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m). #n (elim n) normalize // qed. -theorem commutative_times : commutative nat times. +theorem commutative_times : a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a. #n (elim n) normalize // qed. (* variant sym_times : \forall n,m:nat. n*m = m*n \def symmetric_times. *) -theorem distributive_times_plus : distributive nat times plus. +theorem distributive_times_plus : a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a. #n (elim n) normalize // qed. theorem distributive_times_plus_r : - ∀a,b,c:nat. (b+c)*a = b*a + c*a. + ∀a,b,c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. (ba title="natural plus" href="cic:/fakeuri.def(1)"+/ac)a title="natural times" href="cic:/fakeuri.def(1)"*/aa a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ba title="natural times" href="cic:/fakeuri.def(1)"*/aa a title="natural plus" href="cic:/fakeuri.def(1)"+/a ca title="natural times" href="cic:/fakeuri.def(1)"*/aa. // qed. -theorem associative_times: associative nat times. +theorem associative_times: a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a. #n (elim n) normalize // qed. -lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z). +lemma times_times: ∀x,y,z. xa title="natural times" href="cic:/fakeuri.def(1)"*/a(ya title="natural times" href="cic:/fakeuri.def(1)"*/az) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ya title="natural times" href="cic:/fakeuri.def(1)"*/a(xa title="natural times" href="cic:/fakeuri.def(1)"*/az). // qed. -theorem times_n_1 : ∀n:nat. n = n * 1. +theorem times_n_1 : ∀n: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 n a title="natural times" href="cic:/fakeuri.def(1)"*/a a title="natural number" href="cic:/fakeuri.def(1)"1/a. #n // qed. (* ci servono questi risultati? @@ -182,15 +182,15 @@ qed. (******************** ordering relations ************************) -inductive le (n:nat) : nat → Prop ≝ +inductive le (n: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 ≝ | le_n : le n n - | le_S : ∀ m:nat. le n m → le n (S m). + | le_S : ∀ m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. le n m → le n (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m). interpretation "natural 'less or equal to'" 'leq x y = (le x y). interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)). -definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m. +definition lt: 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 ≝ λn,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 m. interpretation "natural 'less than'" 'lt x y = (lt x y). interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)). @@ -198,16 +198,16 @@ interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)). (* lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m). // qed. *) -definition ge: nat → nat → Prop ≝ λn,m.m ≤ n. +definition ge: 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 ≝ λn,m.m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. interpretation "natural 'greater or equal to'" 'geq x y = (ge x y). -definition gt: nat → nat → Prop ≝ λn,m.m(plus_minus_m_m … Hlecb) /2/ +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/ qed. -theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p. +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. -theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b. -#a #b #c #H @(le_plus_to_le_r … b) /2/ +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/ qed. -theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b. -#a #b #c #H @not_le_to_lt -@(not_to_not … (lt_to_not_le …H)) /2/ +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/ qed. -theorem lt_minus_to_plus_r: ∀a,b,c. a < b - c → a + c < b. -#a #b #c #H @not_le_to_lt @(not_to_not … (le_plus_to_minus …)) -@lt_to_not_le // +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(7)"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 ≤ n → n < p+m → n-m < p. -#n #m #p #lenm #H normalize eq_minus_O /2/ >eq_minus_O // - @monotonic_le_times_r /2/ - |@sym_eq (applyS plus_to_minus) a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a /2/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"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/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/ qed. -theorem minus_plus: ∀n,m,p. n-m-p = n -(m+p). +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). #n #m #p -cases (decidable_le (m+p) n) #Hlt - [@plus_to_minus @plus_to_minus eq_minus_O /2/ >eq_minus_O // +cases (a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a (ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap) n) #Hlt + [@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(9)"eq_minus_O/a /2/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a // ] qed. @@ -978,11 +978,11 @@ theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p). >associative_plus (le_to_leb_true …) // @(transitive_le ? (S m)) /2/ +lemma commutative_min: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/min.def(2)"min/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/ ] qed. -lemma le_minr: ∀i,n,m. i ≤ min n m → i ≤ m. -#i #n #m normalize @leb_elim normalize /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_minl: ∀i,n,m. i ≤ min n m → i ≤ n. +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. /2/ qed. -lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m. -#i #n #m #lein #leim normalize (cases (leb n m)) +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)) normalize // qed. -lemma commutative_max: commutative ? max. -#n #m normalize @leb_elim - [@leb_elim normalize /2/ - |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/ +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/ ] qed. -lemma le_maxl: ∀i,n,m. max n m ≤ i → n ≤ i. -#i #n #m normalize @leb_elim normalize /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_maxr: ∀i,n,m. max n m ≤ i → m ≤ i. +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. /2/ qed. -lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i. -#i #n #m #leni #lemi normalize (cases (leb n m)) +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)) normalize // qed. - -- 2.39.2