[STATEMENT]
lemma mod_tree_lemma1:
  fixes x :: "nat tree"
  assumes "\<forall>i\<in>set_tree y. 0 < i"
  shows "x mod (x + y) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x mod (x + y) = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x mod (x + y) = x
[PROOF STEP]
have "rel_tree (=) (x mod (x + y)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_tree (=) (x mod (x + y)) x
[PROOF STEP]
by applicative_lifting(simp add: assms)
[PROOF STATE]
proof (state)
this:
rel_tree (=) (x mod (x + y)) x

goal (1 subgoal):
 1. x mod (x + y) = x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
rel_tree (=) (x mod (x + y)) x

goal (1 subgoal):
 1. x mod (x + y) = x
[PROOF STEP]
by(unfold tree.rel_eq)
[PROOF STATE]
proof (state)
this:
x mod (x + y) = x

goal:
No subgoals!
[PROOF STEP]
qed