proposition: Lemma det_Vandermonde (R: comRingType) (n:nat) (a: 'rV[R]_n) : \det (Vandermonde n a) = \prod_(i < n) \prod_(j < n | i < j) (a 0 j - a 0 i).
proof: Proof. case: n a => [a|n a]; first by rewrite det_mx00 big1 // => -[] []. exact: det_vander. Qed.
imports: mathcomp(all_ssreflect ssralg perm zmodp) mathcomp(matrix) ssralg_ext