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