proposition: Lemma lfunPn f g : reflect (exists u, f u != g u) (f != g).
proof: Proof. apply: (iffP idP) => [f'g|[x]]; last by apply: contraNneq => /lfunP->. suffices /subvPn[_ /memv_imgP[u _ ->]]: ~~ (limg (f - g) <= 0)%VS. by rewrite lfunE /= lfunE /= memv0 subr_eq0; exists u. apply: contra f'g => /subvP fg0; apply/eqP/lfunP=> u; apply/eqP. by rewrite -subr_eq0 -opp_lfunE -add_lfunE -memv0 fg0 ?memv_img ?memvf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)