proposition: Lemma comp_is_ahom (V : {vspace aT}) (f : 'Hom(rT, sT)) (g : 'Hom(aT, rT)) : ahom_in {:rT} f -> ahom_in V g -> ahom_in V (f \o g).
proof: Proof. move=> /ahom_inP fM /ahom_inP gM; apply/ahom_inP. by split=> [x y Vx Vy|] /=; rewrite !comp_lfunE gM // fM ?memvf. 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)