proposition: Lemma perm_cat2l s1 s2 s3 : perm_eq (s1 ++ s2) (s1 ++ s3) = perm_eq s2 s3.
proof: Proof. apply/permP/permP=> eq23 a; apply/eqP; by move/(_ a)/eqP: eq23; rewrite !count_cat eqn_add2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)