proposition: Lemma skew_yam_consK sha shc i y : is_part sha -> is_skew_yam sha shc (i :: y) -> is_skew_yam sha (decr_nth shc i) y.
proof: Proof. move=> Hpart /(_ _ (hyper_yam_of_eval Hpart)) /=. rewrite /is_yam_of_eval /= => /andP[/andP[Hincr Hyam] /eqP Hc]. apply (is_skew_yamE (hyper_yam_of_eval Hpart)). rewrite /is_yam_of_eval Hyam /= -Hc. by rewrite (incr_nthK (is_part_eval_yam Hyam) Hincr). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab