proposition: Fact lfun_unitrP f g : g * f = 1 /\ f * g = 1 -> lker f == 0%VS.
proof: Proof. case=> _ fK; apply/lker0P; apply: can_inj (g) _ => u. by rewrite -lfun_mulE fK lfunE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)