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