proposition: Lemma is_skew_yamE innev outev z y0 : is_yam_of_eval innev y0 -> is_yam_of_eval outev (z ++ y0) -> is_skew_yam innev outev z.
proof: Proof. move=> Hy0 Hcat y Hy. move: Hy0 Hy Hcat. rewrite /is_yam_of_eval => /andP[Hy0 /eqP <-] /andP[Hy /eqP Hsh] /andP[]. elim: z outev => [| z0 z IHz /=] outev Hcat Hshcat. by rewrite Hy Hsh Hshcat. move: Hcat => /andP[Hincr0 Hcat0]. move/(_ _ Hcat0 (eq_refl _)) : IHz => /andP[-> /eqP->]. by rewrite Hincr0 Hshcat. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab