proposition: Lemma eqseq_catr (T:eqType) (s1 s2 s3: seq T) : (s1 ++ s3 == s2 ++ s3) = (s1 == s2).
proof: Proof. elim/last_ind: s3;first by rewrite !cats0. by move => s x; rewrite -!rcons_cat eqseq_rcons eqxx andbT /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)