# HG changeset patch
# User nipkow
# Date 1362575407 -3600
# Node ID 0c376ef98559a035a94cde93759c3445710d2cc9
# Parent  ac4c1cf1b00113514ffde3464f978c588b069b97
added lemma

diff -r ac4c1cf1b001 -r 0c376ef98559 src/HOL/Library/Extended.thy
--- a/src/HOL/Library/Extended.thy	Wed Mar 06 12:17:52 2013 +0100
+++ b/src/HOL/Library/Extended.thy	Wed Mar 06 14:10:07 2013 +0100
@@ -182,6 +182,9 @@
   apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
   done
 
+lemma Fin_neg_numeral: "Fin(neg_numeral w) = - numeral w"
+by (simp only: Fin_numeral minus_numeral[symmetric] uminus_extended.simps[symmetric])
+
 
 instantiation extended :: (lattice)bounded_lattice
 begin