proposition: Lemma Vl_p1 f E x : slist_E f E -> \1c <=c x -> x <=c (slength f) -> inc (Vl f x) E.
proof: Proof. move => [ha hb] hc hd; move: (ha) => [he _]. apply: hb; apply/(range_gP he). have nN:= (slength_nat ha). case: (equal_or_not x \0c) => xz; first by move: (cltNge clt_01); rewrite - xz. move: (cpred_pr (NS_le_nat hd nN) xz) => [sa sb]. exists (cpred x) => //; apply /(slist_domainP ha). by apply/(cleSlt0P (CS_nat sa) nN); rewrite - sb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)