proposition: Lemma det_vander_k_rec n (a : 'rV[R]_n.+1) (k : nat) (M : 'M[R]_n.+1) : k < n.+1 -> \det (vander_k a M k) = \det (vander_k a M k.-1).
proof: Proof. move=> kn. destruct k as [|k] => //=. rewrite /lc /= (@determinant_multilinear _ _ _ (\matrix_i (if i == inord (n.+1 - k.+1) then row (inord i) (vander_k a M k) else row (inord i) (vander_k a M k.+1))) (\matrix_i (if i == inord (n.+1 - k.+1) then row (inord i.-1) (vander_k a M k) else row (inord i) (vander_k a M k.+1))) (inord (n.+1 - k.+1)) 1 (- a``_ord0)); last 3 first. rewrite scale1r !rowK eqxx vander_k_rec //; last first. by rewrite subSS leq_subr. by rewrite ltnW. rewrite subSS. rewrite leq_subr andbT subn_eq0. case: ifPn => [nk|]. by move: (leq_ltn_trans nk kn); rewrite ltnn. rewrite -ltnNge => kn'. rewrite leqnn /lc inordK; last by rewrite ltnS leq_subr. rewrite vander_k_rec //; last 2 first. rewrite ltnW //; by apply: (ltn_trans kn'). by rewrite leq_subr. rewrite subn_eq0 leqNgt kn' /= leq_subr andbT leq_subLR addnBA; last first. by rewrite ltnW. rewrite addnC. rewrite -addnBA // subnn addn0 ltnn vander_k_rec //; last 2 first. by rewrite ltnW // ltnS ltnW. by rewrite -subnS leq_subr. rewrite -subnS subn_eq0. rewrite ltnS in kn, kn'. case: ifPn. rewrite -subn_eq0 => /eqP ->. rewrite (_ : inord 0 = 0) // ?scaleNr //. apply/val_inj => //=. by rewrite inordK. rewrite -ltnNge => k1n. case: ifPn => //. case/andP. rewrite subnS subSn; last by rewrite ltnW. by rewrite ltnNge leq_pred. by rewrite scaleNr. apply/matrixP => i j; by rewrite !mxE eq_sym (negbTE (neq_lift _ _)) mxE inord_val. apply/matrixP => i j; by rewrite !mxE eq_sym (negbTE (neq_lift _ _)) mxE inord_val. rewrite mul1r (_ : \matrix_i _ = vander_k a M k); last first. apply/matrixP => i j; rewrite !mxE. case: ifPn => [/eqP Hi|Hi]. rewrite !mxE (_ : inord i = i) //. apply/val_inj => /=. by rewrite inordK. rewrite vander_k_rec //; last first. by rewrite -ltnS. by rewrite ltnW. case: ifPn => i0. transitivity ((row (inord i) (vander_k a M k)) 0 j); last first. rewrite mxE (_ : inord i = i) //. apply/val_inj => /=. by rewrite inordK. rewrite vander_k_rec //; last 2 first. by rewrite (leq_trans _ kn) // -addn2 leq_addr. by rewrite -ltnS. by rewrite i0. rewrite -(ltnS i) ltn_ord andbT. case: ifPn => nki. rewrite /lc. transitivity ((row (inord i) (vander_k a M k)) 0 j); last first. rewrite mxE (_ : inord i = i) //. apply/val_inj => /=. by rewrite inordK. rewrite vander_k_rec //; last 2 first. by rewrite ltnW // ltnW. by rewrite -ltnS. rewrite (negbTE i0) -(ltnS i) ltn_ord andbT. have {nki} : n.+1 - k.+1 < i. rewrite ltn_neqAle nki andbT. apply: contra Hi => /eqP ->. apply/eqP/val_inj => /=. by rewrite inordK //. rewrite subnS -ltnS prednK; last by rewrite lt0n subn_eq0 -ltnNge ltnW. by rewrite ltnS => ->. transitivity ((row (inord i) (vander_k a M k)) 0 j); last first. rewrite mxE (_ : inord i = i) //. apply/val_inj => /=. by rewrite inordK. rewrite vander_k_rec //; last 2 first. by rewrite ltnW // ltnW. by rewrite -ltnS. rewrite (negbTE i0) -(ltnS i) ltn_ord andbT. have /negbTE -> // : ~~ (n.+1 - k <= i). apply: contra nki. apply: leq_trans. rewrite leq_subLR addnC. destruct n as [|n] => //. rewrite subSn; last by rewrite -ltnS ltnW. by rewrite addSn addnS subnK // -ltnS ltnW. rewrite (_ : \det (\matrix_i _) = 0) ?mulr0 ?addr0 //. have H : inord (n.+1 - k.+1) != inord (n.+1 - k.+2) :> 'I_n.+1. apply/eqP => /(congr1 (fun x => nat_of_ord x)) /=. rewrite 2!subSS. rewrite inordK // ?ltnS ?leq_subr //. rewrite inordK // ?ltnS ?leq_subr //. destruct n as [|n] => //. rewrite !subSS. move/(congr1 (fun x => x + k)%N). rewrite subnK; last by rewrite ltnW. rewrite addnC addnBA // addnC. rewrite addnK -{2}(addn0 n). rewrite -addn1 => /eqP. by rewrite eqn_add2l. apply (@determinant_alternate _ _ _ (inord (n.+1 - k.+1)) (inord (n.+1 - k.+2))) => //. move=> i. rewrite !mxE eqxx eq_sym (negbTE H) 2!subSS. rewrite inordK; last by rewrite ltnS leq_subr. rewrite inordK; last by rewrite ltnS leq_subr. rewrite -subnS [in LHS]vander_k_rec // ?leq_subr //; last by rewrite ltnW // ltnW. rewrite subn_eq0. case: ifPn => // nk2. rewrite (_ : n - k.+1 = 0)%N //; last by apply/eqP; rewrite subn_eq0. by rewrite vander_k_rec // ltnW // ltnW. rewrite andbT (_ : _ <= _ = false); last first. rewrite -(leq_add2r k.+1) subnK //. rewrite addnC addnBA; last by rewrite ltnW // ltnW. rewrite addnC -addnBA; last by rewrite -addn1 leq_addr. rewrite subSn // subnn // addn1. apply/negbTE. by rewrite -leqNgt. rewrite [in RHS]vander_k_rec // ?leq_subr //; last by rewrite ltnW. rewrite subn_eq0 (negbTE nk2) andbT (_ : _ <= _ = false) //. rewrite -(leq_add2r k.+1) subnK //; last by rewrite ltnW. by rewrite subnK ?ltnn. Qed.
imports: mathcomp(all_ssreflect ssralg perm zmodp) mathcomp(matrix) ssralg_ext