proposition: Lemma permut_app : forall p q, permut (p ++ q) (q ++ p).
proof: Proof. intros l1 l2. assert (H1: length l2 + length l1 = length (l1 ++ l2)). rewrite app_length. apply Nat.add_comm. assert (H2: length (l1 ++ l2) = length l1 + length l2). apply app_length. simple refine (Permut _ _ _ _ _ _). - rewrite 2!app_length. apply Nat.add_comm. - intros k. apply (cast_ord H1). apply unsplit. destruct (split (cast_ord H2 k)) as [k'|k']. now right. now left. - apply injective_split with (f := fun k => match k with inl k' => inr k' | inr k' => inl k' end). clear. intros [k1|k1] [k2|k2] ; try easy ; intros H ; injection H ; apply f_equal. - simpl. intros n. case splitP ; simpl ; change ssrnat.addn with plus ; intros k Hk. rewrite onth_app_l. rewrite onth_app_r by lia. rewrite Nat.add_comm, Nat.add_sub. now rewrite <- Hk. eapply elimT. now apply ssrnat.ltP. now rewrite Hk. rewrite onth_app_r by lia. rewrite onth_app_l. now rewrite Hk, Nat.add_comm, Nat.add_sub. cut (n < length l1 + length l2). lia. eapply elimT. apply ssrnat.ltP. now rewrite <- app_length. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)