proposition: Lemma qpoly_inv0 : qpoly_inv 0%R = 0%R :> {poly %/ h}.
proof: Proof. rewrite /qpoly_inv /= coprimep0 -size_poly_eq1. rewrite [in X in X == _]mk_monicE. by have [[]] := hI; case: size => [|[]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(div bigop binomial finset finfun ssralg countalg finalg) mathcomp(poly polydiv qpoly perm fingroup falgebra fieldext finfield galois) mathcomp(finalg zmodp matrix vector)