proposition: Lemma eqlfunP f g v : reflect (f v = g v) (v \in lker (f - g)).
proof: Proof. by rewrite memv_ker !lfun_simp subr_eq0; apply: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)