proposition: Lemma sizeT_qf (p : polyF) : rpoly p -> qf_cps xpredT (sizeT p).
proof: Proof. elim: p => /= [_|c p ihp /andP[rc rq]]; first exact: qf_cps_ret. apply: qf_cps_bind; first exact: ihp. move=> [|n] //= _; last exact: qf_cps_ret. by apply: qf_cps_if; rewrite //= rc. 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)