proposition: Fact poly_intro_unit p q : q * p = 1 -> p \in poly_unit.
proof: Proof. move=> pq1; apply/andP; split; last first. apply/unitrP; exists q`_0. by rewrite 2!mulrC -!/(coefp 0 _) -rmorphM pq1 rmorph1. have: size (q * p) == 1 by rewrite pq1 size_poly1. have [-> | nz_p] := eqVneq p 0; first by rewrite mulr0 size_poly0. have [-> | nz_q] := eqVneq q 0; first by rewrite mul0r size_poly0. rewrite size_mul // (polySpred nz_p) (polySpred nz_q) addnS addSn !eqSS. by rewrite addn_eq0 => /andP[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)