proposition: Lemma isnull_qf (p : polyF) : rpoly p -> qf_cps xpredT (isnull p).
proof: Proof. move=> rp; apply: qf_cps_bind; first exact: sizeT_qf. by move=> ? _; apply: qf_cps_ret. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)