proposition: Fact aspace_cap_subproof A B : algid A \in B -> is_aspace (A :&: B).
proof: Proof. move=> BeA; apply/andP. split; [apply/has_algidP | by rewrite subv_cap !prodv_sub ?capvSl ?capvSr]. exists (algid A); rewrite /is_algid algid_neq0 memv_cap memv_algid. by split=> // u /memv_capP[Au _]; rewrite ?algidl ?algidr. 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)