proposition: Lemma eqseq_cat1 (T: Type) (s1 s2 s3: seq T) : (s3 ++ s1 = s3 ++ s2) -> (s1 = s2).
proof: Proof. by elim s3 => // a l h; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)