tuned proof;

--- a/src/HOL/Auth/KerberosIV.thy	Thu Oct 29 13:21:38 2009 +0100
+++ b/src/HOL/Auth/KerberosIV.thy	Thu Oct 29 14:53:53 2009 +0100
@@ -780,7 +780,7 @@
 lemma u_NotexpiredSK_NotexpiredAK:
      "\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
       \<Longrightarrow> \<not> expiredAK Ta evs"
-  by (metis nat_add_commute le_less_trans)
+  by (metis le_less_trans)
 
 
 subsection{* Reliability: friendly agents send something if something else happened*}