proposition: Lemma alt_add1_0 (m : 'X_{1..n}) i : (nth 0%N m i).+1 = nth 0%N m i.+1 -> 'a_(m + rho) = 0.
proof: Proof. Proof using . move=> Heq. have Hi1n : i.+1 < n. rewrite ltnNge; apply/negP => Hi. by move: Heq; rewrite [RHS]nth_default // size_tuple. have Hi : i < n by rewrite ltnW. pose i0 := Ordinal Hi; pose i1 := Ordinal Hi1n. have /alt_alternate : i0 != i1. apply/negP => /eqP/(congr1 val)/=/eqP. by rewrite ieqi1F. apply. rewrite !mnmDE !mnmE !(mnm_nth 0%N) -Heq -(mnm_nth 0%N m i0). rewrite addSn -addnS subn1 /= subnS prednK //. have -> : (n.-1 - i = n - i.+1)%N. case: n Hi1n Hi {i0 i1} => [//= | n' _] /=. by rewrite subSS. by rewrite subn_gt0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition mathcomp(matrix)