proposition: Lemma limg0 f : (f @: 0 = 0)%VS.
proof: Proof. by rewrite limg_line linear0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)