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