proposition: Lemma sorted_is_flattened leT (Htrans : transitive leT) (Hanti : antisymmetric leT) (Hrefl : reflexive leT) : forall n (l k : seq A), n = size l -> uniq l -> sorted leT l -> sorted leT k -> {subset k <= l} -> k = flatten (map (fun elt => filter (pred1 elt) k) l).
proof: Proof. elim=> [[]// k _ _ _ Hk H|] /=. destruct k => //. exfalso. move: (H s). by rewrite !inE eqxx orTb in_nil => /(_ isT). move=> n0 IH [|hd tl] // v [lst_sz] lst_uniq lst_sorted v_sorted Hincl. have X1 : v = filter (pred1 hd) v ++ filter (predC (pred1 hd)) v. apply: (@sorted_eq _ leT) => //. - apply: sorted_cat. + exact: sorted_filter. + exact: sorted_filter. + move=> a. rewrite mem_filter => /andP[/= /eqP ?]; subst hd => av b. rewrite mem_filter => /andP[/= ba /Hincl]. rewrite inE => /orP[|]. * move/eqP => ?; by subst b. * move=> btl. rewrite /sorted in lst_sorted. have /= := @subseq_path _ _ Htrans a [:: b] tl. rewrite andbT. by apply => //; rewrite sub1seq. - by rewrite perm_sym; apply permEl, perm_filterC. rewrite {1}X1 {X1} /=. congr (_ ++ _). move: lst_uniq => /= /andP[hdtl tl_uniq]. rewrite (IH tl (filter (predC (pred1 hd)) v) lst_sz tl_uniq). - congr flatten. apply eq_in_map => i i_tl. rewrite -filter_predI. apply eq_in_filter => j j_v /=. case/boolP: (j == i) => ij //=. apply/negP => /eqP ?; subst j. move/eqP : ij => ?; subst i. by rewrite i_tl in hdtl. - destruct tl => //=. by case/andP : lst_sorted. - exact: sorted_filter. - move=> i. rewrite mem_filter /= => /andP[ihd] /Hincl. by rewrite inE => /orP[|//]; rewrite (negbTE ihd). Qed.
imports: mathcomp(all_ssreflect fingroup perm)