proposition: Lemma rgcdpTP (k : polyF -> fF) : (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) -> forall p q e, qf_eval e (rgcdpT p q k) = qf_eval e (k (lift (rgcdp (eval_poly e p) (eval_poly e q)))).
proof: Proof. move=> Pk p q e; rewrite /rgcdpT /rgcdp !sizeTP /=. case: (_ < _); rewrite !isnullP /=; case: (_ == _); rewrite -?Pk ?sizeTP; by rewrite ?rgcdp_loopP. 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)