fact: Definition lfun_simp := (comp_lfunE, scale_lfunE, opp_lfunE, add_lfunE, sum_lfunE, lfunE).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)