[STATEMENT]
lemma size_size_new: "\<lbrakk>invar (big :: 'a state); 0 < size big\<rbrakk> \<Longrightarrow> 0 < size_new big"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar big; 0 < size big\<rbrakk> \<Longrightarrow> 0 < size_new big
[PROOF STEP]
by(induction big)(auto simp: size_size_new)