proposition: Lemma lead_coefT_qf (p : polyF) : rpoly p -> qf_cps (@rterm _) (lead_coefT p).
proof: Proof. elim: p => [_|c q ihp //= /andP[rc rq]]; first by apply: qf_cps_ret. apply: qf_cps_bind => [|y ty]; first exact: ihp. by apply: qf_cps_if; rewrite //= ty. 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)