proposition: Lemma skew_field_module_semisimple A M : let sumA X := (\sum_(x <- X) A * <[x]>)%VS in (A * M <= M)%VS -> {X | [/\ sumA X = M, directv (sumA X) & 0 \notin X]}.
proof: Proof. move=> sumA sAM_M; pose X := Nil aT; pose k := (\dim (A * M) - \dim (sumA X))%N. have: (\dim (A * M) - \dim (sumA X) < k.+1)%N by []. have: [/\ (sumA X <= A * M)%VS, directv (sumA X) & 0 \notin X]. by rewrite /sumA directvE /= !big_nil sub0v dimv0. elim: {X k}k.+1 (X) => // k IHk X [sAX_AM dxAX nzX]; rewrite ltnS => leAXk. have [sM_AX | /subvPn/sig2W[y My notAXy]] := boolP (M <= sumA X)%VS. by exists X; split=> //; apply/eqP; rewrite eqEsubv (subv_trans sAX_AM). have nz_y: y != 0 by rewrite (memPnC notAXy) ?mem0v. pose AY := sumA (y :: X). have sAY_AM: (AY <= A * M)%VS by rewrite [AY]big_cons subv_add ?prodvSr. have dxAY: directv AY. rewrite directvE /= !big_cons [_ == _]directv_addE dxAX directvE eqxx /=. rewrite -/(sumA X) eqEsubv sub0v andbT -limg_amulr. apply/subvP=> _ /memv_capP[/memv_imgP[a Aa ->]]/[!lfunE]/= AXay. rewrite memv0 (mulIr_eq0 a (mulIr _)) ?fieldT //. apply: contraR notAXy => /fieldT-Ua; rewrite -[y](mulKr Ua) /sumA. by rewrite -big_distrr -(prodv_id A) /= -prodvA big_distrr memv_mul ?memvV. apply: (IHk (y :: X)); first by rewrite !inE eq_sym negb_or nz_y. rewrite -subSn ?dimvS // (directvP dxAY) /= big_cons -(directvP dxAX) /=. rewrite subnDA (leq_trans _ leAXk) ?leq_sub2r // leq_subLR -add1n leq_add2r. by rewrite dim_cosetv_unit ?fieldT ?adim_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)