proposition: Lemma vander_lastE n (a : 'rV[R]_n.+1) : vander_last a = vander_k a (vander a) n.
proof: Proof. apply/row_matrixP => i. rewrite {2}(_ : i = inord i); last first. apply/val_inj => /=. by rewrite inordK. rewrite vander_k_rec //; last by rewrite -ltnS. case: ifPn => i0. rewrite /vander_last. apply/rowP => j. rewrite !mxE. case: ifP => //. move/eqP => abs; exfalso. apply abs. apply/val_inj => /=. by move/eqP : i0. rewrite subSn // subnn lt0n i0 /= -ltnS ltn_ord /= /lc /vander_last; apply/rowP => j. rewrite !mxE. case: ifP => [|i0']. move/eqP/(congr1 (fun x => nat_of_ord x)) => /= abs; exfalso. move/eqP : i0; by apply. case: ifP => [|j0]. move=> /eqP ->. rewrite -exprS inordK // inordK; last first. by rewrite (leq_trans _ (ltn_ord i)) // ltnS leq_pred. rewrite prednK; last first. by rewrite lt0n. by rewrite (_ : 0 = ord0) // subrr. rewrite inordK // inordK // (ltn_trans _ (ltn_ord i)) // -subn1. by rewrite -{2}(subn0 i) ltn_sub2l // lt0n. Qed.
imports: mathcomp(all_ssreflect ssralg perm zmodp) mathcomp(matrix) ssralg_ext