proposition: Lemma eq_inv_skew_dominate (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2) (u1 v1 : seq T1) (u2 v2 : seq T2) s : eq_inv (u1 ++ v1) (u2 ++ v2) -> size u1 = size u2 -> skew_dominate s u1 v1 -> skew_dominate s u2 v2.
proof: Proof. move/eq_invP; rewrite !size_cat => [] [Hsz Hinv] Hszu /dominateP[Hsz1 Hdom]. apply/dominateP; split => [| i Hi1]. move: Hsz Hsz1; rewrite !size_drop !leq_subLR Hszu => /eqP. by rewrite eqn_add2l => /eqP ->. have Hi2 : i < size (drop s u1) by move: Hi1; rewrite !size_drop Hszu. move/(_ _ Hi2) : Hdom. rewrite !nth_drop !ltNge; apply contra. move : Hi1 Hi2; rewrite !size_drop !ltn_subRL => Hi2 Hi1. have -> : nth inh u1 (s + i) = nth inh (u1 ++ v1) (s + i) by rewrite nth_cat Hi1. have -> : nth inh u2 (s + i) = nth inh (u2 ++ v2) (s + i) by rewrite nth_cat Hi2. have -> : nth inh v1 i = nth inh (u1 ++ v1) (size u1 + i) by rewrite nth_cat ltnNge leq_addr /= addKn. have -> : nth inh v2 i = nth inh (u2 ++ v2) (size u2 + i) by rewrite nth_cat ltnNge leq_addr /= addKn. rewrite {}Hinv Hszu //. rewrite leq_add2r ltn_add2l; apply/andP; split. - by apply ltnW; apply: (leq_ltn_trans _ Hi2); exact: leq_addr. - by move: Hi1 Hsz1; rewrite size_drop -ltn_subRL => /leq_trans /[apply]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab