proposition: Lemma size_subseq_leqif s1 s2 : subseq s1 s2 -> size s1 <= size s2 ?= iff (s1 == s2).
proof: Proof. move=> sub12; split; first exact: size_subseq. apply/idP/eqP=> [|-> //]; case/subseqP: sub12 => m sz_m ->{s1}. rewrite size_mask -sz_m // -all_count -(eq_all eqb_id). by move/(@all_pred1P _ true)->; rewrite sz_m mask_true. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)