From f5b55b3e3395ec39a1429468ae833dbff72158c4 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 29 Feb 2012 11:31:22 +0000 Subject: [PATCH] commit by user andrea --- weblib/arithmetics/nat.ma | 46 +++++++++++++++++++-------------------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma index 24cfc5ef6..226050632 100644 --- a/weblib/arithmetics/nat.ma +++ b/weblib/arithmetics/nat.ma @@ -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). -/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. +(* /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a/span/span/ *) #n @a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a // qed. (* variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def @@ -945,7 +945,7 @@ 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(10)"le_plus_to_minus/a span class="error" title="Parse error: illegal begin of statement"/span +#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"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. @@ -979,11 +979,11 @@ theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p). >associative_plus