proposition: Lemma limg_span f X : (f @: <<X>> = <<map f X>>)%VS.
proof: Proof. by rewrite !span_def big_map limg_sum; apply: eq_bigr => x _; rewrite limg_line. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)