proposition: Lemma redivpTP (k : nat * polyF * polyF -> fF) : (forall c qq r e, qf_eval e (k (c,qq,r)) = qf_eval e (k (c, lift (eval_poly e qq), lift (eval_poly e r)))) -> forall p q e (d := redivp (eval_poly e p) (eval_poly e q)), qf_eval e (redivpT p q k) = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).
proof: Proof. move=> Pk p q e /=; rewrite isnullP unlock /=. case q0 : (eval_poly e q == 0) => /=; first by rewrite Pk /= mul0r add0r polyC0. rewrite !sizeTP lead_coefTP /=; last by move=> *; rewrite !redivp_rec_loopTP. rewrite redivp_rec_loopTP /=; last by move=> *; rewrite Pk. by rewrite mul0r add0r polyC0 redivp_rec_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)