--- a/src/GeneralRec.v	Thu Mar 29 17:15:14 2012 -0400
+++ b/src/GeneralRec.v	Thu Mar 29 18:10:52 2012 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2006, 2011, Adam Chlipala
+(* Copyright (c) 2006, 2011-2012, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -346,6 +346,11 @@
 
 Require Import Max.
 
+Theorem max_spec_le : forall n m, n <= m /\ max n m = m \/ m <= n /\ max n m = n.
+  induction n; destruct m; simpl; intuition;
+    specialize (IHn m); intuition.
+Qed.
+
 Ltac max := intros n m; generalize (max_spec_le n m); crush.
 
 Lemma max_1 : forall n m, max n m >= n.