proposition: Lemma algid_subproof U : {e | e \in U & has_algid U ==> (U <= lker (amull e - 1) :&: lker (amulr e - 1))%VS}.
proof: Proof. apply: sig2W; case: has_algidP => [[e]|]; last by exists 0; rewrite ?mem0v. case=> Ae _ idAe; exists e => //; apply/subvP=> u /idAe[eu_u ue_u]. by rewrite memv_cap !memv_ker !lfun_simp /= eu_u ue_u subrr eqxx. 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)