proposition: Lemma dim_cosetv U x : x != 0 -> \dim (U * <[x]>) = \dim U.
proof: Proof. move=> nz_x; rewrite -limg_amulr limg_dim_eq //. apply/eqP; rewrite -subv0; apply/subvP=> y. by rewrite memv_cap memv0 memv_ker lfunE mulf_eq0 (negPf nz_x) orbF => /andP[]. 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)