proposition: Lemma limg_comp f g U : ((g \o f) @: U = g @: (f @: U))%VS.
proof: Proof. have /andP[/eqP <- _] := vbasisP U; rewrite !limg_span; congr (span _). by rewrite -map_comp; apply/eq_map => u; rewrite lfunE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)