proposition: Lemma Vfirst_position_aux_nth : forall n (ys : vector A n) k i j (hj : j<n), Vfirst_position_aux k ys = Some i -> P (Vnth ys hj) -> i <= k+j.
proof: Proof. induction ys as [|y n ys]; intros k i j hj; simpl. discr. destruct (P_dec y). intro h; inversion h; clear h; subst. destruct j as [|j]; lia. intro h1. destruct j as [|j]; intro h2. fo. gen (IHys _ _ _ _ h1 h2). lia. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)