proposition: Lemma exchange_head_foot: forall A (head : A) body foot, exchange ((head :: body) ++ (foot :: nil)) 0 (length (head :: body)) = ((foot :: body) ++ (head :: nil)).
proof: Proof. intros. apply nth_error_eq. intro i. case (eq_nat_dec i 0); intro. + subst i. rewrite nth_error_exchange; simpl. 2: lia. rewrite nth_error_app2. simpl. rewrite Nat.sub_diag. trivial. trivial. rewrite app_length. simpl. lia. + case (eq_nat_dec i (length (head :: body))); intro. - subst i. rewrite nth_error_exchange'; simpl. 2: lia. rewrite nth_error_app2. rewrite Nat.sub_diag. trivial. trivial. rewrite app_length. simpl. lia. - rewrite nth_error_exchange''; auto. destruct i. contradiction. simpl. simpl in n0. assert (i < (length body) \/ i >= length (body ++ (foot :: nil))). { rewrite app_length. simpl. lia. } destruct H. repeat rewrite nth_error_app1; auto. assert (i >= length (body ++ (head :: nil))). { rewrite app_length in *. simpl in *. trivial. } apply nth_error_None in H. apply nth_error_None in H0. congruence. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset