proposition: Lemma path_drop : forall (s: seq nat) (i j d x : nat), path ltn x s -> i < j -> path ltn (nth d (x :: s) i) (drop i.+1 (x :: s)).
proof: Proof. elim => [ | hd tl hi] //= [ | i] j d x /andP [hx hp] hij /=. - by rewrite hx. by apply: (hi _ j.-1 _ hd) => //; move: hij; case: j. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor