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