proposition: Lemma position_aux_plus x j k : forall l i, position_aux i x l = Some k -> position_aux (i+j) x l = Some (k+j).
proof: Proof. induction l; simpl. discr. case_beq x a; intros. inversion H. refl. assert (S(i+j) = S i+j). refl. rewrite H1. apply IHl. hyp. Qed.
imports: Coq(Arith Lia) CoLoR(ListUtil BoolUtil EqUtil LogicUtil)