proposition: Lemma rgcdpTs_qf (ps : seq polyF) : all rpoly ps -> qf_cps rpoly (rgcdpTs ps).
proof: Proof. elim: ps => [_|c p ihp /andP[rc rp]] //=; first exact: qf_cps_ret. by apply: qf_cps_bind => [|r rr]; [apply: ihp|apply: rgcdpT_qf]. 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)