[STATEMENT]
lemma Pdrop_valid [simp]: "valid_path (ldropn n P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (ldropn n P)
[PROOF STEP]
using valid_path_drop
[PROOF STATE]
proof (prove)
using this:
valid_path ?P \<Longrightarrow> valid_path (ldropn ?n ?P)

goal (1 subgoal):
 1. valid_path (ldropn n P)
[PROOF STEP]
by auto