proposition: Lemma comp_lfun0r f : (f \o 0)%VF = 0 :> 'Hom(aT, rT).
proof: Proof. by apply/lfunP=> u; do !rewrite lfunE /=; rewrite linear0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)