proposition: Lemma Vnth_first_position_aux : forall n (ys : vector A n) k i (hi : i-k < n), Vfirst_position_aux k ys = Some i -> P (Vnth ys hi).
proof: Proof. induction ys as [|y n ys IH]; intros k i hi; simpl Vfirst_position_aux. discr. destruct (P_dec y). intro h; inversion h; clear h; subst. rewrite Vnth_cons. destruct (lt_ge_dec 0 (i-i)). lia. hyp. intro h. rewrite Vnth_cons. destruct (lt_ge_dec 0 (i-k)). assert (hi' : i - S k < n). lia. gen (IH _ _ hi' h); intro hx. rewrite Vnth_eq with (h2:=hi'). hyp. lia. gen (Vfirst_position_aux_ge _ _ h). lia. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)