proposition: Lemma Vfirst_position_aux_ge : forall n (ys : vector A n) k i, Vfirst_position_aux k ys = Some i -> i >= k.
proof: Proof. induction ys as [|y n ys]; intros k i; simpl. discr. destruct (P_dec y). 2: firstorder auto with arith. intro h; inversion h; clear h; subst. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)