[STATEMENT]
lemma pmdl_closed_red:
  assumes "pmdl B \<subseteq> pmdl A" and "p \<in> pmdl A" and "red B p q"
  shows "q \<in> pmdl A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> pmdl A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> pmdl A
[PROOF STEP]
have "q - p \<in> pmdl A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q - p \<in> pmdl A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q - p \<in> ?A
 2. ?A \<subseteq> pmdl A
[PROOF STEP]
have "p - q \<in> pmdl B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p - q \<in> pmdl B
[PROOF STEP]
by (rule red_diff_in_pmdl, fact)
[PROOF STATE]
proof (state)
this:
p - q \<in> pmdl B

goal (2 subgoals):
 1. q - p \<in> ?A
 2. ?A \<subseteq> pmdl A
[PROOF STEP]
hence "- (p - q) \<in> pmdl B"
[PROOF STATE]
proof (prove)
using this:
p - q \<in> pmdl B

goal (1 subgoal):
 1. - (p - q) \<in> pmdl B
[PROOF STEP]
by (rule pmdl.span_neg)
[PROOF STATE]
proof (state)
this:
- (p - q) \<in> pmdl B

goal (2 subgoals):
 1. q - p \<in> ?A
 2. ?A \<subseteq> pmdl A
[PROOF STEP]
thus "q - p \<in> pmdl B"
[PROOF STATE]
proof (prove)
using this:
- (p - q) \<in> pmdl B

goal (1 subgoal):
 1. q - p \<in> pmdl B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q - p \<in> pmdl B

goal (1 subgoal):
 1. pmdl B \<subseteq> pmdl A
[PROOF STEP]
qed fact
[PROOF STATE]
proof (state)
this:
q - p \<in> pmdl A

goal (1 subgoal):
 1. q \<in> pmdl A
[PROOF STEP]
from pmdl.span_add[OF this \<open>p \<in> pmdl A\<close>]
[PROOF STATE]
proof (chain)
picking this:
q - p + p \<in> pmdl A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q - p + p \<in> pmdl A

goal (1 subgoal):
 1. q \<in> pmdl A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q \<in> pmdl A

goal:
No subgoals!
[PROOF STEP]
qed