proposition: Lemma nth_error_ok_in : forall (A : Type) n (l : list A) (a : A), nth_error l n = Some a -> {l1 : list A & {l2 : list A | length l1 = n /\ l = l1 ++ a :: l2}}.
proof: Proof. intros A n l; generalize n; clear n; induction l as [ | a' l]. intros n a; rewrite nth_error_nil; intros; discriminate. intros [ | n] a; simpl; intros H. injection H; intro; subst a'. exists (@nil A); exists l; split; trivial. destruct (IHl n a H) as [l1 [l2 [L H']]]. exists (a' :: l1); exists l2; simpl; split; subst; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)