proposition: Lemma position_aux_ok2 i x : forall l k, element_at l k = Some x -> exists k', k' <= k /\ position_aux i x l = Some (i+k').
proof: Proof. induction l; simpl; intros. discr. case_beq x a. exists 0. intuition. rewrite (beq_ko beq_ok) in H0. destruct k. inversion H. subst. cong. destruct (IHl _ H). exists (S x0). intuition. rewrite Nat.add_succ_r. simpl. apply position_aux_S. hyp. Qed.
imports: Coq(Arith Lia) CoLoR(ListUtil BoolUtil EqUtil LogicUtil)