proposition: Lemma subseq_anti : antisymmetric subseq.
proof: Proof. move=> s1 s2 /andP[] /size_subseq_leqif /leqifP. by case: eqP => [//|_] + /size_subseq; rewrite ltnNge => /negP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)