proposition: Lemma rgcdp_loopP (k : polyF -> fF) : (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) -> forall n p q e, qf_eval e (rgcdp_loopT n p q k) = qf_eval e (k (lift (rgcdp_loop n (eval_poly e p) (eval_poly e q)))).
proof: Proof. move=> Pk n p q e; elim: n => /= [| m IHm] in p q e *; rewrite redivpTP /==> *; rewrite ?isnullP ?eval_lift -/(rmodp _ _); by case: (_ == _); do ?by rewrite -?Pk ?IHm ?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)