proposition: Lemma ahomWin (f : ahom aT rT) U : ahom_in U f.
proof: Proof. by apply/ahom_inP; split; [apply: in2W (rmorphM _) | apply: rmorph1]. 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)