proposition: Lemma mulVz : {in unitz, left_inverse 1%R invz *%R}.
proof: Proof. by move=> n /pred2P[] ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)