proposition: Lemma nth_error_remove : forall (A : Type) (a : A) k k' n, nth_error (k ++ a :: k') (if le_lt_dec (length k) n then S n else n) = nth_error (k ++ k') n.
proof: Proof. intros A b k; induction k as [ | a k]; intros k' m. simpl; trivial. simpl length; simpl app. destruct m as [ | m]. simpl; trivial. generalize (IHk k' m); destruct (le_lt_dec (length k) m) as [k_le_m | k_gt_m]; destruct (le_lt_dec (S (length k)) (S m)) as [k_le_m' | k_gt_m']. simpl; trivial. absurd (S m <= m); auto with arith; apply Nat.lt_le_trans with (length k); auto with arith. absurd (S m <= m); auto with arith; apply Nat.lt_le_trans with (length k); auto with arith. simpl; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)