--- a/Precedence_ord.thy	Tue Dec 22 23:13:31 2015 +0800
+++ b/Precedence_ord.thy	Wed Jan 06 20:46:14 2016 +0800
@@ -14,6 +14,19 @@
                                    (Prc fx sx, Prc fy sy) \<Rightarrow> 
                                  fx < fy \<or> (fx \<le> fy \<and> sy \<le> sx))"
 
+lemma preced_leI1[intro]: 
+  assumes "fx < fy"
+  shows "Prc fx sx \<le> Prc fy sy"
+  using assms
+  by (simp add: precedence_le_def) 
+
+lemma preced_leI2[intro]: 
+  assumes "fx \<le> fy"
+  and "sy \<le> sx"
+  shows "Prc fx sx \<le> Prc fy sy"
+  using assms
+  by (simp add: precedence_le_def) 
+
 definition
   precedence_less_def: "x < y \<longleftrightarrow> (case (x, y) of
                                (Prc fx sx, Prc fy sy) \<Rightarrow>