proposition: Lemma eqseq_cat_simp (T:eqType) (s1 s3: seq T) : (s1 ++ s3 == s3) = (nilp s1).
proof: Proof. by rewrite -{2}(cat0s s3) eqseq_catr - size_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)