proposition: Lemma polyCV c : c%:P^-1 = (c^-1)%:P.
proof: Proof. have [/rmorphV-> // | nUc] := boolP (c \in GRing.unit). by rewrite !invr_out // poly_unitE coefC (negbTE nUc) andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)