proposition: Lemma det_vander_k_vander n (a : 'rV[R]_n.+1) (k : nat) : k <= n.+1 -> \det (vander_k a (vander a) k) = \det (vander a).
proof: Proof. elim: k => // k IH. rewrite ltnS => kn. by rewrite det_vander_k // IH // ltnW. Qed.
imports: mathcomp(all_ssreflect ssralg perm zmodp) mathcomp(matrix) ssralg_ext