proposition: Lemma permut_app_r : forall p q r, permut p r -> permut (p ++ q) (r ++ q).
proof: Proof. intros p q r H. apply permut_trans with (q ++ r). apply permut_trans with (q ++ p). apply permut_app. now apply permut_app_l. apply permut_app. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)