X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=weblib%2Fflagtest%2Fprova.ma;h=cf8a896676a6d9c7cf704680fa28432c4b10a200;hb=e305a62a7cb0a49fea3d241474e4c5bcd40e7272;hp=64490b74c452b9a27927fcc033810a7ed661a610;hpb=0a331eb559f571081a3f78df13b5c75b25595ead;p=helm.git diff --git a/weblib/flagtest/prova.ma b/weblib/flagtest/prova.ma index 64490b74c..cf8a89667 100644 --- a/weblib/flagtest/prova.ma +++ b/weblib/flagtest/prova.ma @@ -1 +1,1121 @@ -(* script *) \ No newline at end of file +<<<<<<< .mine +(* scriptino *)======= +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "basics/relations.ma". + +inductive nat : Type[0] â + | O : nat + | S : nat â nat. + +interpretation "Natural numbers" 'N = nat. + +alias num (instance 0) = "natural number". + +definition pred â + λ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 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 : 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: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: 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: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: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: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: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: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 â 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: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. + +(* +theorem plus_Sn_m: ân,m:nat. S (n + m) = S n + m. +// qed. +*) + +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: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. + +(* +theorem plus_Sn_m1: ân,m:nat. S m + n = n + S m. +#n (elim n) normalize // qed. +*) + +(* deleterio? +theorem plus_n_1 : ân:nat. S n = n+1. +// qed. +*) + +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 : 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 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: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 +\def injective_plus_r. + +theorem injective_plus_l: âm:nat.injective nat nat (λn.n+m). +/2/ qed. *) + +(* theorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m +\def injective_plus_l. *) + +(*************************** times *****************************) + +let rec times n 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: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: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: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: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 : 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 : 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: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: 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. 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: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? +theorem times_O_to_O: ân,m:nat.n*m=O â n=O ⨠m=O. +napply nat_elim2 /2/ +#n #m #H normalize #H1 napply False_ind napply not_eq_O_S +// qed. + +theorem times_n_SO : ân:nat. n = n * S O. +#n // qed. + +theorem times_SSO_n : ân:nat. n + n = (S(S O)) * n. +normalize // qed. + +nlemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)). +// qed. + +theorem or_eq_eq_S: \forall n.\exists m. +n = (S(S O))*m \lor n = S ((S(S O))*m). +#n (elim n) + ##[@ /2/ + ##|#a #H nelim H #b#ornelim or#aeq + ##[@ b @ 2 // + ##|@ (S b) @ 1 /2/ + ##] +qed. +*) + +(******************** ordering relations ************************) + +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: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: 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)). + +(* lemma eq_lt: ân,m. (n < m) = (S n ⤠m). +// qed. *) + +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: 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.ma title="natural 'less than'" href="cic:/fakeuri.def(1)"</an. + +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/ +qed. + +(* +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. + +(* +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. + +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. + +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. + +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. + +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. + +(* this are instances of the le versions +theorem lt_S_S_to_lt: ân,m. S n < S m â n < m. +/2/ qed. + +theorem lt_to_lt_S_S: ân,m. n < m â S n < S m. +/2/ qed. *) + +theorem lt_to_not_zero : â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/not_zero.def(1)"not_zero/a m. +#n #m #Hlt (elim Hlt) // qed. + +(* lt vs. le *) +theorem not_le_Sn_O: â 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 a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. +#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. + +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. + +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. + +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. + +(* this is le_S_S_to_le +theorem lt_S_to_le: ân,m:nat. n < S m â n ⤠m. +/2/ qed. +*) + +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. + +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/ + ] +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. + +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. + +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. + +(* 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. + +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. + +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. + +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. + +(* +theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat. +(S O) \lt n \to O \lt (pred n). +intros. +apply (ltn_to_ltO (pred (S O)) (pred n) ?). + apply (lt_pred (S O) n) + [ apply (lt_O_S O) + | assumption + ] +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/ +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. +#n #posn (cases posn) // +qed. + +(* +theorem lt_pred: \forall n,m. + O < n \to n < m \to pred n < pred m. +apply nat_elim2 + [intros.apply False_ind.apply (not_le_Sn_O ? H) + |intros.apply False_ind.apply (not_le_Sn_O ? H1) + |intros.simplify.unfold.apply le_S_S_to_le.assumption + ] +qed. + +theorem le_pred_to_le: + ân,m. O < m â pred n ⤠pred m â n ⤠m. +intros 2 +elim n +[ apply le_O_n +| simplify in H2 + rewrite > (S_pred m) + [ apply le_S_S + assumption + | assumption + ] +]. +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. + +(* 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. + +(*not lt +theorem eq_to_not_lt: âa,b:nat. a = b â a â® b. +intros. +unfold Not. +intros. +rewrite > H in H1. +apply (lt_to_not_eq b b) +[ assumption +| reflexivity +] +qed. + +theorem lt_n_m_to_not_lt_m_Sn: ân,m. n < m â m â® S n. +intros +unfold Not +intro +unfold lt in H +unfold lt in H1 +generalize in match (le_S_S ? ? H) +intro +generalize in match (transitive_le ? ? ? H2 H1) +intro +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(5)"le_to_or_lt_eq/a ?? Hle) // +#Heq /3/ 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. + +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. + +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. + +(* 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/ +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. + +(* +(* other abstract properties *) +theorem antisymmetric_le : antisymmetric nat le. +unfold antisymmetric.intros 2. +apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))). +intros.apply le_n_O_to_eq.assumption. +intros.apply False_ind.apply (not_le_Sn_O ? H). +intros.apply eq_f.apply H. +apply le_S_S_to_le.assumption. +apply le_S_S_to_le.assumption. +qed. + +theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m +\def antisymmetric_le. + +theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ân,m. n ⤠m â m < S n â n=m. +intros +unfold lt in H1 +generalize in match (le_S_S_to_le ? ? H1) +intro +apply antisym_le +assumption. +qed. +*) + +(* well founded induction principles *) + +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/ +(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 *) + |#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/ + ] +qed. + +(* some properties of functions *) + +definition increasing â λ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. ân:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. f n 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 n). + +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/ +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/ +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/ +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(5)"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,2,0)"S/a a)) % // + ] + ] +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(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/ + ] +qed. + +(*********************** monotonicity ***************************) +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. + +(* +theorem le_plus_r: âp,n,m:nat. n ⤠m â p + n ⤠p + m +â monotonic_le_plus_r. *) + +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. + +(* +theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p +\def monotonic_le_plus_l. *) + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +(* 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. + +(* +variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def +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. + +(* +variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def +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. + +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. + +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. + +(* +theorem le_to_lt_to_lt_plus: âa,b,c,d:nat. +a ⤠c â b < d â a + b < c+d. +(* bello /2/ un po' lento *) +#a #b #c #d #leac #lebd +normalize napplyS le_plus // qed. +*) + +(* times *) +theorem monotonic_le_times_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 times" href="cic:/fakeuri.def(1)"*/a m). +#n #x #y #lexy (elim n) normalize//(* lento /2/*) +#a #lea @a href="cic:/matita/arithmetics/nat/le_plus.def(7)"le_plus/a // +qed. + +(* +theorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m +\def monotonic_le_times_r. *) + +(* +theorem monotonic_le_times_l: +âm:nat.monotonic nat le (λn.n*m). +/2/ qed. +*) + +(* +theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p +\def monotonic_le_times_l. *) + +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/ +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. + +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/ + |#n #m #H #lta #le + @a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a @H /2/ + ] +qed. + +(* +theorem le_S_times_2: ân,m.O < m â n ⤠m â S n ⤠2*m. +#n #m #posm #lenm (* interessante *) +applyS (le_plus n m) // qed. *) + +(* times & lt *) +(* +theorem lt_O_times_S_S: ân,m:nat.O < (S n)*(S m). +intros.simplify.unfold lt.apply le_S_S.apply le_O_n. +qed. *) + +(* +theorem lt_times_eq_O: \forall a,b:nat. +O < a â a * b = O â b = O. +intros. +apply (nat_case1 b) +[ intros. + reflexivity +| intros. + rewrite > H2 in H1. + rewrite > (S_pred a) in H1 + [ apply False_ind. + apply (eq_to_not_lt O ((S (pred a))*(S m))) + [ apply sym_eq. + assumption + | apply lt_O_times_S_S + ] + | assumption + ] +] +qed. + +theorem O_lt_times_to_O_lt: \forall a,c:nat. +O \lt (a * c) \to O \lt a. +intros. +apply (nat_case1 a) +[ intros. + rewrite > H1 in H. + simplify in H. + assumption +| intros. + apply lt_O_S +] +qed. + +lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m. +intros. +elim (le_to_or_lt_eq O ? (le_O_n m)) + [assumption + |apply False_ind. + rewrite < H1 in H. + rewrite < times_n_O in H. + apply (not_le_Sn_O ? H) + ] +qed. *) + +(* +theorem monotonic_lt_times_r: +ân:nat.monotonic nat lt (λm.(S n)*m). +/2/ +simplify. +intros.elim n. +simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption. +apply lt_plus.assumption.assumption. +qed. *) + +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/ + |#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/ +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(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(9)"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(10)"lt_to_le_to_lt_times/a/2/ +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/ +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. + +(* +theorem nat_compare_times_l : \forall n,p,q:nat. +nat_compare p q = nat_compare ((S n) * p) ((S n) * q). +intros.apply nat_compare_elim.intro. +apply nat_compare_elim. +intro.reflexivity. +intro.absurd (p=q). +apply (inj_times_r n).assumption. +apply lt_to_not_eq. assumption. +intro.absurd (q
nat_compare_n_n.reflexivity.
+intro.apply nat_compare_elim.intro.
+absurd (p minus_Sn_m.
+apply le_S.assumption.
+apply lt_to_le.assumption.
+qed.
+
+theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
+intros.
+apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
+intro.elim n1.simplify.apply le_n_Sn.
+simplify.rewrite < minus_n_O.apply le_n.
+intros.simplify.apply le_n_Sn.
+intros.simplify.apply H.
+qed.
+
+theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
+intros 3.intro.
+(* autobatch *)
+(* end auto($Revision: 9739 $) proof: TIME=1.33 SIZE=100 DEPTH=100 *)
+apply (trans_le (m-n) (S (m-(S n))) p).
+apply minus_le_S_minus_S.
+assumption.
+qed.
+
+theorem le_minus_m: \forall n,m:nat. n-m \leq n.
+intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)).
+intros.rewrite < minus_n_O.apply le_n.
+intros.simplify.apply le_n.
+intros.simplify.apply le_S.assumption.
+qed.
+
+theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
+intros.apply (lt_O_n_elim n H).intro.
+apply (lt_O_n_elim m H1).intro.
+simplify.unfold lt.apply le_S_S.apply le_minus_m.
+qed.
+
+theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
+intros 2.
+apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)).
+intros.apply le_O_n.
+simplify.intros. assumption.
+simplify.intros.apply le_S_S.apply H.assumption.
+qed.
+*)
+
+(* monotonicity and galois *)
+
+theorem monotonic_le_minus_l:
+â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 â qa title="natural minus" href="cic:/fakeuri.def(1)"-/an a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"â¤/a pa title="natural minus" href="cic:/fakeuri.def(1)"-/an.
+@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/
+ ]
+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(6)"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/
+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.
+
+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 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 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 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(7)"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(7)"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(7)"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(6)"le_plus_minus_m_m/a ? q)) /2/
+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/
+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(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. 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 (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.
+
+(*
+theorem plus_minus: ân,m,p. p ⤠m â (n+m)-p = n +(m-p).
+#n #m #p #lepm @plus_to_minus >(commutative_plus p)
+>associative_plus