proposition: Lemma Fadjoin_eq_sum : <<K; x>>%VS = sumKx.
proof: Proof. apply/esym/eqP; rewrite eqEdim eq_leq ?andbT. apply/subv_sumP=> i _; rewrite -agenvM prodvS ?subv_adjoin //. by rewrite -expv_line (subv_trans (subX_agenv _ _)) ?agenvS ?addvSr. rewrite dim_Fadjoin -[n]card_ord -sum_nat_const (directvP Fadjoin_sum_direct). by apply: eq_bigr => i _; rewrite /= dim_cosetv. 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)