proposition: Lemma rgdcop_recTP (k : polyF -> fF) : (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) -> forall p q n e, qf_eval e (rgdcop_recT n p q k) = qf_eval e (k (lift (rgdcop_rec (eval_poly e p) (eval_poly e q) n))).
proof: Proof. move=> Pk p q n e; elim: n => [|n Pn] /= in k Pk p q e *. rewrite isnullP /=. by case: (_ == _); rewrite Pk /= mul0r add0r ?(polyC0, polyC1). rewrite /rcoprimep rgcdpTP ?sizeTP ?eval_lift => * /=. case: (_ == _); by do ?[rewrite /= ?(=^~Pk, redivpTP, rgcdpTP, sizeTP, Pn, eval_lift) //==> *]. do ?[rewrite /= ?(=^~Pk, redivpTP, rgcdpTP, sizeTP, Pn, eval_lift) //==> *]. case: (_ == _); by do ?[rewrite /= ?(=^~Pk, redivpTP, rgcdpTP, sizeTP, Pn, eval_lift) //==> *]. 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)