proposition: Lemma Vfirst_position_nth : forall n (ys : vector A n) i j (hj : j<n), Vfirst_position ys = Some i -> P (Vnth ys hj) -> i <= j.
proof: Proof. intros n ys i j hj. apply Vfirst_position_aux_nth. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)