proposition: Lemma Fadjoin_sum_direct : directv sumKx.
proof: Proof. rewrite directvE /=; case: (ubnPgeq n) (isT : n > 0) => -[//|m] ltmn _. elim: m ltmn => [|m IHm] ltm1n; rewrite ?big_ord1 // !(big_ord_recr m.+1) /=. do [move/(_ (ltnW ltm1n))/eqP; set S := (\sum_i _)%VS] in IHm *. rewrite -IHm dimv_add_leqif; apply/subvP=> z; rewrite memv_cap => /andP[Sz]. case/memv_cosetP=> y Ky Dz; rewrite memv0 Dz mulf_eq0 expf_eq0 /=. apply: contraLR ltm1n => /norP[nz_y nz_x]. rewrite -leqNgt -(leq_pmul2r (adim_gt0 K)) -dim_Fadjoin. have{IHm} ->: (m.+1 * \dim K)%N = \dim S. rewrite -[m.+1]card_ord -sum_nat_const IHm. by apply: eq_bigr => i; rewrite dim_cosetv ?expf_neq0. apply/dimvS/agenv_sub_modl; first by rewrite (sumv_sup 0) //= prodv1 sub1v. rewrite prodvDl subv_add -[S]big_distrr prodvA prodv_id subvv !big_distrr /=. apply/subv_sumP=> i _; rewrite -expv_line prodvCA -expvSl expv_line. have [ltim | lemi] := ltnP i m; first by rewrite (sumv_sup (Sub i.+1 _)). have{lemi} /eqP->: i == m :> nat by rewrite eqn_leq leq_ord. rewrite -big_distrr -2!{2}(prodv_id K) /= -!prodvA big_distrr -/S prodvSr //=. by rewrite -(canLR (mulKf nz_y) Dz) -memvE memv_mul ?rpredV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)