proposition: Lemma is_tableau_sorted_dominate t : is_tableau t = [&& is_part (shape t), all (sorted <=%O) t & sorted (fun (r s : seq T) => dominate s r) t].
proof: Proof. Proof using. apply/idP/idP; elim: t => [// | t0 t IHt]. - move=> /=/and4P[Hnnil Hrow0 Hdom /IHt /and3P[Hpart Hall Hsort]]. rewrite {}Hpart {}Hrow0 {}Hall {IHt} !andbT /=; apply/andP; split. + case: t Hdom {Hsort} => [_ | t1 t] /=; first by case: t0 Hnnil. by move => /dominateP[]. + by case: t Hdom Hsort => [// | t1 t]/= -> ->. - move=>/and3P[Hpart]. have:= part_head_non0 Hpart. rewrite [head _ _]/= [all _ _]/= [is_tableau _]/=. move=> /nilP /eqP-> /andP[-> Hall Hsort /=]. apply/andP; split. + by case: t Hsort {Hpart Hall IHt} => [// | t1 t] /= /andP[]. + apply: IHt; rewrite (is_part_consK Hpart) Hall /=. exact: (sorted_consK Hsort). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted