proposition: Lemma perm_cat s1 s2 t1 t2 : perm_eq s1 s2 -> perm_eq t1 t2 -> perm_eq (s1 ++ t1) (s2 ++ t2).
proof: Proof. by move=> /perm_catr-> /perm_catl->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)