[STATEMENT]
lemma pos_les_eq_append_diff [simp]:
  "p \<le>\<^sub>p q \<Longrightarrow> p @ (q -\<^sub>p p) = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le>\<^sub>p q \<Longrightarrow> p @ q -\<^sub>p p = q
[PROOF STEP]
by (metis option.sel pos_diff_def position_less_eq_def remove_prefix_append)