proposition: Lemma position_aux_ok1 k x : forall l i, position_aux i x l = Some k -> k >= i /\ element_at l (k-i) = Some x.
proof: Proof. induction l; simpl. discr. case_beq x a. intros. inversion H. rewrite Nat.sub_diag. intuition. destruct l. simpl. discr. intros. ded (IHl _ H0). assert (exists p', k - i = S p'). exists (k-i-1). lia. destruct H2. rewrite H2. assert (k - S i = x0). lia. rewrite <- H3. intuition. Qed.
imports: Coq(Arith Lia) CoLoR(ListUtil BoolUtil EqUtil LogicUtil)