[STATEMENT]
lemma order_impl_root_order: "\<lbrakk>k > 0; order k t\<rbrakk> \<Longrightarrow> root_order k t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; order k t\<rbrakk> \<Longrightarrow> root_order k t
[PROOF STEP]
apply(cases t)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>0 < k; order k t; t = Leaf x1\<rbrakk> \<Longrightarrow> root_order k t
 2. \<And>x21 x22. \<lbrakk>0 < k; order k t; t = Node x21 x22\<rbrakk> \<Longrightarrow> root_order k t
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done