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